From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 17:31:25 +0100
Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was
 simplified

---
 interp/constrexpr_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrexpr_ops.ml')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d48ea4d07..161fd1eb1d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -178,7 +178,7 @@ and args_eq (a1,e1) (a2,e2) =
   Option.equal (eq_located explicitation_eq) e1 e2 &&
   constr_expr_eq a1 a2
 
-and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   constr_expr_eq e1 e2 &&
   Option.equal (eq_located Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
-- 
cgit v1.2.3


From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 16:19:51 +0100
Subject: CLEANUP: removing unused field

I have removed the second field of the "Constrexpr.CRecord" variant
because once it was set to "None"
it never changed to anything else.
It was just carried and copied around.
---
 interp/constrexpr_ops.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'interp/constrexpr_ops.ml')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 161fd1eb1d..a97e8e6db7 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 =
       Option.equal Int.equal proj1 proj2 &&
       constr_expr_eq e1 e2 &&
       List.equal args_eq al1 al2
-  | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+  | CRecord (_, l1), CRecord (_, l2) ->
     let field_eq (r1, e1) (r2, e2) =
       eq_reference r1 r2 && constr_expr_eq e1 e2
     in
-    Option.equal constr_expr_eq e1 e2 &&
     List.equal field_eq l1 l2
   | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
       (** Don't care about the case_style *)
@@ -238,7 +237,7 @@ let constr_loc = function
   | CLetIn (loc,_,_,_) -> loc
   | CAppExpl (loc,_,_) -> loc
   | CApp (loc,_,_) -> loc
-  | CRecord (loc,_,_) -> loc
+  | CRecord (loc,_) -> loc
   | CCases (loc,_,_,_,_) -> loc
   | CLetTuple (loc,_,_,_,_) -> loc
   | CIf (loc,_,_,_,_) -> loc
-- 
cgit v1.2.3


From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 20 Jan 2016 17:25:10 +0100
Subject: Update copyright headers.

---
 interp/constrexpr_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrexpr_ops.ml')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 2d48ea4d07..1644700268 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 13 Mar 2016 13:18:10 +0100
Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments.

---
 interp/constrexpr_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrexpr_ops.ml')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9c577034e8..c5730e6261 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 =
       Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
       eq_reference c1 c2 &&
-      List.equal cases_pattern_expr_eq a1 a2 &&
+      Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
       List.equal cases_pattern_expr_eq b1 b2
   | CPatAtom(_,r1), CPatAtom(_,r2) ->
       Option.equal eq_reference r1 r2
-- 
cgit v1.2.3