diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 06262f85016146a1e84bda7aabd214fa1a33f602..79f8e4978406798c1221ae3887e41e39da0d2565 100644
--- a/theories/algebra/base.v
+++ b/theories/algebra/base.v
@@ -1,6 +1,8 @@
 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.
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index e3fd5407518ba00c02e012b2e09cb1bae211f8ed..3c1ee03036d68b90bad769d3941e634b7aa1fbd2 100644
--- a/theories/heap_lang/lang.v
+++ b/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)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 1198fb520ac2490fd90ca8390bb499a2dd0f47c2..b047b1a75bacc28e5f7b49d602425d3e01bd83c1 100644
--- a/theories/heap_lang/tactics.v
+++ b/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