Merge branch 'master' into gen_proofmode

theories/algebra/base.v

 From mathcomp Require Export ssreflect.
 From stdpp Require Export prelude.
 Set Default Proof Using "Type".
+(* Reset options set by the ssreflect plugin to their defaults *)
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
+Global Unset Asymmetric Patterns.
 Ltac done := stdpp.tactics.done.

theories/heap_lang/lang.v

@@ -91,7 +91,7 @@ Bind Scope val_scope with val.
 
 Fixpoint of_val (v : val) : expr :=
   match v with
-  | RecV f x e _ => Rec f x e
+  | RecV f x e => Rec f x e
   | LitV l => Lit l
   | PairV v1 v2 => Pair (of_val v1) (of_val v2)
   | InjLV v => InjL (of_val v)

theories/heap_lang/tactics.v

@@ -39,7 +39,7 @@ Inductive expr :=
 Fixpoint to_expr (e : expr) : heap_lang.expr :=
   match e with
   | Val v e' _ => e'
-  | ClosedExpr e _ => e
+  | ClosedExpr e => e
   | Var x => heap_lang.Var x
   | Rec f x e => heap_lang.Rec f x (to_expr e)
   | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
@@ -100,7 +100,7 @@ Ltac of_expr e :=
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
-  | Val _ _ _ | ClosedExpr _ _ => true
+  | Val _ _ _ | ClosedExpr _ => true
   | Var x => bool_decide (x ∈ X)
   | Rec f x e => is_closed (f :b: x :b: X) e
   | Lit _ => true
@@ -147,7 +147,7 @@ Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
 Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
   match e with
   | 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
   | Rec f y e =>
      Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e