Commit 24ea529a authored by Robbert Krebbers's avatar Robbert Krebbers

`Unset Asymmetric Patterns`.

This is an old flag set by the ssr plugin, and recently unset in coq-stdpp,
see https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/issues/5.
parent 650261fc
From mathcomp Require Export ssreflect. From mathcomp Require Export ssreflect.
From stdpp Require Export prelude. From stdpp Require Export prelude.
Set Default Proof Using "Type". Set Default Proof Using "Type".
(* Reset options set by the ssreflect plugin to their defaults *)
Global Set Bullet Behavior "Strict Subproofs". Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope. Global Open Scope general_if_scope.
Global Unset Asymmetric Patterns.
Ltac done := stdpp.tactics.done. Ltac done := stdpp.tactics.done.
...@@ -91,7 +91,7 @@ Bind Scope val_scope with val. ...@@ -91,7 +91,7 @@ Bind Scope val_scope with val.
Fixpoint of_val (v : val) : expr := Fixpoint of_val (v : val) : expr :=
match v with match v with
| RecV f x e _ => Rec f x e | RecV f x e => Rec f x e
| LitV l => Lit l | LitV l => Lit l
| PairV v1 v2 => Pair (of_val v1) (of_val v2) | PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v) | InjLV v => InjL (of_val v)
......
...@@ -39,7 +39,7 @@ Inductive expr := ...@@ -39,7 +39,7 @@ Inductive expr :=
Fixpoint to_expr (e : expr) : heap_lang.expr := Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with match e with
| Val v e' _ => e' | Val v e' _ => e'
| ClosedExpr e _ => e | ClosedExpr e => e
| Var x => heap_lang.Var x | Var x => heap_lang.Var x
| Rec f x e => heap_lang.Rec f x (to_expr e) | Rec f x e => heap_lang.Rec f x (to_expr e)
| App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2) | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
...@@ -100,7 +100,7 @@ Ltac of_expr e := ...@@ -100,7 +100,7 @@ Ltac of_expr e :=
Fixpoint is_closed (X : list string) (e : expr) : bool := Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with match e with
| Val _ _ _ | ClosedExpr _ _ => true | Val _ _ _ | ClosedExpr _ => true
| Var x => bool_decide (x X) | Var x => bool_decide (x X)
| Rec f x e => is_closed (f :b: x :b: X) e | Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ => true | Lit _ => true
...@@ -147,7 +147,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed. ...@@ -147,7 +147,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr := Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with match e with
| Val v e H => Val v e H | Val v e H => Val v e H
| ClosedExpr e H => @ClosedExpr e H | ClosedExpr e => ClosedExpr e
| Var y => if decide (x = y) then es else Var y | Var y => if decide (x = y) then es else Var y
| Rec f y e => | Rec f y e =>
Rec f y $ if decide (BNamed x f BNamed x y) then subst x es e else e Rec f y $ if decide (BNamed x f BNamed x y) then subst x es e else e
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment