From 8f5d447769a41cd251701272a6ff71a7a20de658 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 11:36:12 +0100
Subject: Improving the API of constrexpr_ops.mli.

Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.

Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.

So, there is also a "fix" of semantic here.
---
 parsing/g_constr.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 47455f9842..7316a4335a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -231,7 +231,7 @@ GEXTEND Gram
 
   record_field_declaration:
     [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
-      (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
+      (id, mkCLambdaN (!@loc) (binders_of_lidents params) c) ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-- 
cgit v1.2.3


From 45a411377244da33111cf5d7002df70de912bc64 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 11:57:58 +0100
Subject: Factorizing/unifying code in dealing with binders.

Note: This reveals a little bug yet to fix in g_vernac.ml4. In

Definition f '((x,y):id nat * id nat) '((x',y'):id nat * id nat) := Eval unfold id in x+y = x'+y'.

the "id" are wrongly unfolded and in

Definition f '(x,y) '(x',y') := x+y = x'+y' : Prop.

an unexpected cast remains in the body of f.
---
 parsing/g_vernac.ml4 | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 18807113c9..ba441a662f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -243,16 +243,22 @@ GEXTEND Gram
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
-      let (bl, c) = expand_pattern_binders mkCLambdaN bl c in
-      (match c with
-          CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
+      if List.exists (function LocalPattern _ -> true | _ -> false) bl
+      then
+        (* FIXME: "red" will be applied to types in bl and Cast with remain *)
+        let c = mkCLambdaN (!@loc) bl c in
+	DefineBody ([], red, c, None)
+      else
+        (match c with
+        | CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
         let ((bl, c), tyo) =
           if List.exists (function LocalPattern _ -> true | _ -> false) bl
           then
+            (* FIXME: "red" will be applied to types in bl and Cast with remain *)
             let c = CCast (!@loc, c, CastConv t) in
-            (expand_pattern_binders mkCLambdaN bl c, None)
+            (([],mkCLambdaN (!@loc) bl c), None)
           else ((bl, c), Some t)
         in
 	DefineBody (bl, red, c, tyo)
-- 
cgit v1.2.3


From ac655f3c8eb348b84c5ba3e3ed41977d36849ea5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 06:55:32 +0100
Subject: Removing a redundant line in the syntax of record fields.

---
 parsing/g_constr.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 7316a4335a..22d4c68c35 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -223,7 +223,6 @@ GEXTEND Gram
 
   record_fields:
     [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
-      | f = record_field_declaration; ";" -> [f]
       | f = record_field_declaration -> [f]
       | -> []
     ] ]
-- 
cgit v1.2.3


From d2830ca4adf062df96d5e8978d4254cf5ece30c4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 12:12:39 +0100
Subject: Supporting arbitrary binders in record fields, including e.g.
 patterns.

---
 parsing/g_constr.ml4 | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 22d4c68c35..e461db85f9 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -44,9 +44,6 @@ let binder_of_name expl (loc,na) =
 let binders_of_names l =
   List.map (binder_of_name Explicit) l
 
-let binders_of_lidents l =
-  List.map (fun (loc, id) -> binder_of_name Explicit (loc, Name id)) l
-
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
   let ty = match tyc with
       Some ty -> ty
@@ -229,8 +226,8 @@ GEXTEND Gram
   ;
 
   record_field_declaration:
-    [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
-      (id, mkCLambdaN (!@loc) (binders_of_lidents params) c) ] ]
+    [ [ id = global; bl = binders; ":="; c = lconstr ->
+      (id, mkCLambdaN (!@loc) bl c) ] ]
   ;
   binder_constr:
     [ [ "forall"; bl = open_binders; ","; c = operconstr LEVEL "200" ->
-- 
cgit v1.2.3