From 24ea529ae1482999ee248292c263049f5ce74711 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 14 Nov 2017 01:11:19 +0100
Subject: [PATCH] `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.
---
 theories/algebra/base.v      | 2 ++
 theories/heap_lang/lang.v    | 2 +-
 theories/heap_lang/tactics.v | 6 +++---
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/theories/algebra/base.v b/theories/algebra/base.v
index 06262f850..79f8e4978 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 e3fd54075..3c1ee0303 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 1198fb520..b047b1a75 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
-- 
GitLab