From 80d36bc6538b7feaab3dfa43f6e234ae85b55692 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 07:27:06 +0100
Subject: A test checking for non-collision of name in irrefutable patterns.

---
 test-suite/output/PatternsInBinders.out | 2 ++
 test-suite/output/PatternsInBinders.v   | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index c012a86b01..95be04c32c 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
+fun (pat : nat) '(x, y) => x + y = pat
+     : nat -> nat * nat -> Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 6fa357a90c..0bad472f41 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
 
 End Suboptimal.
+
+(** Test risk of collision for internal name *)
+Check fun pat => fun '(x,y) => x+y = pat.
-- 
cgit v1.2.3


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.
---
 dev/doc/changes.txt       |  7 +++++++
 interp/constrexpr_ops.ml  | 18 +++---------------
 interp/constrexpr_ops.mli | 12 ++++++------
 parsing/g_constr.ml4      |  2 +-
 plugins/funind/indfun.ml  |  6 +++---
 vernac/command.ml         |  2 +-
 6 files changed, 21 insertions(+), 26 deletions(-)

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 03742fb8ad..688f72a216 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -33,6 +33,13 @@ The following type aliases where removed
 
 The module Constrarg was merged into Stdarg.
 
+In Constrexpr_ops:
+
+  Deprecating abstract_constr_expr in favor of mkCLambdaN, and
+  prod_constr_expr in favor of mkCProdN. Note: the first ones were
+  interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
+  ones were preserving the original sharing of the type.
+
 ** Ltac API **
 
 Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 59c24900d2..7433336f8f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -363,21 +363,9 @@ let mkCLambdaN loc bll c =
   let (bll, c) = expand_pattern_binders loop bll c in
   loop loc bll c
 
-let rec abstract_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::bl ->
-      List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
-      (abstract_constr_expr c bl)
-  | LocalPattern _::_ -> assert false
-
-let rec prod_constr_expr c = function
-  | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
-  | LocalRawAssum (idl,bk,t)::bl ->
-      List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
-      (prod_constr_expr c bl)
-  | LocalPattern _::_ -> assert false
+(* Deprecated *)
+let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c
+let prod_constr_expr c bl =  mkCProdN (local_binders_loc bl) bl c
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index a92da035f6..7d3011a6e1 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -49,14 +49,14 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
 val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr
 val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
-val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
-val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
-
 val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr
-(** Same as [abstract_constr_expr], with location *)
-
 val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
-(** Same as [prod_constr_expr], with location *)
+
+(** @deprecated variant of mkCLambdaN *)
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+
+(** @deprecated variant of mkCProdN *)
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
 val expand_pattern_binders :
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" ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99b04898ba..94b6b912d3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -151,7 +151,7 @@ let build_newrecursive
   let (rec_sign,rec_impls) =
     List.fold_left
       (fun (env,impls) (((_,recname),_),bl,arityc,_) ->
-        let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
+        let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
 	let evdref = ref (Evd.from_env env0) in
 	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
@@ -436,7 +436,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
 let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
-  let type_of_f = Constrexpr_ops.prod_constr_expr ret_type args in
+  let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in
   let rec_arg_num =
     let names =
       List.map
@@ -467,7 +467,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
-  let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in
+  let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in
   let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type
       nb_args relation =
     try
diff --git a/vernac/command.ml b/vernac/command.ml
index 4b4f4d2711..62a5b97151 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -262,7 +262,7 @@ match local with
     (gr,inst,Lib.is_modtype_strict ())
 
 let interp_assumption evdref env impls bl c =
-  let c = prod_constr_expr c bl in
+  let c = mkCProdN (local_binders_loc bl) bl c in
   interp_type_evars_impls env evdref ~impls c
 
 let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
-- 
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.
---
 interp/constrexpr_ops.ml  | 68 +++++++++++++++++------------------------------
 interp/constrexpr_ops.mli |  3 ---
 parsing/g_vernac.ml4      | 14 +++++++---
 3 files changed, 34 insertions(+), 51 deletions(-)

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7433336f8f..223ec15472 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -301,67 +301,47 @@ let add_name_in_env env n =
 
 let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
 
-let expand_pattern_binders mkC bl c =
-  let rec loop bl c =
+let expand_binders mkC loc bl c =
+  let rec loop loc bl c =
     match bl with
-    | [] -> ([], [], c)
+    | [] -> ([], c)
     | b :: bl ->
-        let (env, bl, c) = loop bl c in
         match b with
-        | LocalRawDef (n, _) ->
+        | LocalRawDef ((loc1,_) as n, b) ->
+            let env, c = loop (Loc.merge loc1 loc) bl c in
             let env = add_name_in_env env n in
-            (env, b :: bl, c)
-        | LocalRawAssum (nl, _, _) ->
+            (env, CLetIn (loc,n,b,c))
+        | LocalRawAssum ((loc1,_)::_ as nl, bk, t) ->
+            let env, c = loop (Loc.merge loc1 loc) bl c in
             let env = List.fold_left add_name_in_env env nl in
-            (env, b :: bl, c)
-        | LocalPattern (loc, p, ty) ->
+            (env, mkC loc (nl,bk,t) c)
+        | LocalRawAssum ([],_,_) -> loop loc bl c
+        | LocalPattern (loc1, p, ty) ->
+            let env, c = loop (Loc.merge loc1 loc) bl c in
             let ni = Hook.get fresh_var env c in
-            let id = (loc, Name ni) in
-            let b =
-              LocalRawAssum
-                ([id], Default Explicit,
-                 match ty with
+            let id = (loc1, Name ni) in
+            let ty = match ty with
                  | Some ty -> ty
-                 | None -> CHole (loc, None, IntroAnonymous, None))
+                 | None -> CHole (loc1, None, IntroAnonymous, None)
             in
-            let e = CRef (Libnames.Ident (loc, ni), None) in
+            let e = CRef (Libnames.Ident (loc1, ni), None) in
             let c =
               CCases
                 (loc, LetPatternStyle, None, [(e,None,None)],
-                 [(loc, [(loc,[p])], mkC loc bl c)])
+                 [(loc1, [(loc1,[p])], c)])
             in
-            (ni :: env, [b], c)
+            (ni :: env, mkC loc ([id],Default Explicit,ty) c)
   in
-  let (_, bl, c) = loop bl c in
-  (bl, c)
+  let (_, c) = loop loc bl c in
+  c
 
 let mkCProdN loc bll c =
-  let rec loop loc bll c =
-    match bll with
-    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-        CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | LocalRawDef ((loc1,_) as id,b) :: bll ->
-        CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
-    | [] -> c
-    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalPattern (loc,p,ty) :: bll -> assert false
-  in
-  let (bll, c) = expand_pattern_binders loop bll c in
-  loop loc bll c
+  let mk loc b c = CProdN (loc,[b],c) in
+  expand_binders mk loc bll c
 
 let mkCLambdaN loc bll c =
-  let rec loop loc bll c =
-    match bll with
-    | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
-        CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
-    | LocalRawDef ((loc1,_) as id,b) :: bll ->
-        CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
-    | [] -> c
-    | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
-    | LocalPattern (loc,p,ty) :: bll -> assert false
-  in
-  let (bll, c) = expand_pattern_binders loop bll c in
-  loop loc bll c
+  let mk loc b c = CLambdaN (loc,[b],c) in
+  expand_binders mk loc bll c
 
 (* Deprecated *)
 let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 7d3011a6e1..9d154340f4 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -59,9 +59,6 @@ val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t
-val expand_pattern_binders :
-  (Loc.t -> local_binder list -> constr_expr -> constr_expr) ->
-  local_binder list -> constr_expr -> local_binder list * constr_expr
 
 (** {6 Destructors}*)
 
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(-)

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 ++-----
 test-suite/success/record_syntax.v | 8 ++++++++
 2 files changed, 10 insertions(+), 5 deletions(-)

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" ->
diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v
index db2bbb0dc7..07a5bc0606 100644
--- a/test-suite/success/record_syntax.v
+++ b/test-suite/success/record_syntax.v
@@ -45,3 +45,11 @@ Record Foo := { foo : unit; }.
 Definition foo_ := {| foo := tt; |}.
 
 End E.
+
+Module F.
+
+Record Foo := { foo : nat * nat -> nat -> nat }.
+
+Definition foo_ := {| foo '(x,y) n := x+y+n |}.
+
+End F.
-- 
cgit v1.2.3


From 01622922a3a68cc4a0597bb08e0f7ba5966a7144 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Dec 2016 12:53:08 +0100
Subject: Documenting the grammar {| ... |} syntax for building records.

And an extra minor changes (use of zeroone when relevant, use of type
rather than term).
---
 doc/common/macros.tex     |  3 ++-
 doc/refman/RefMan-ext.tex | 24 +++++++++++++++++++-----
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 5abdecfc18..0a4251a373 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -145,7 +145,7 @@
 
 \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}}
 \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}}
-
+\newcommand{\typecstrtype}{\zeroone{{\tt :}~{\type}}}
 
 \newcommand{\Fwterm}{\nterm{Fwterm}}
 \newcommand{\Index}{\nterm{index}}
@@ -164,6 +164,7 @@
 \newcommand{\digit}{\nterm{digit}}
 \newcommand{\exteqn}{\nterm{ext\_eqn}}
 \newcommand{\field}{\nterm{field}}
+\newcommand{\fielddef}{\nterm{field\_def}}
 \newcommand{\firstletter}{\nterm{first\_letter}}
 \newcommand{\fixpg}{\nterm{fix\_pgm}}
 \newcommand{\fixpointbodies}{\nterm{fix\_bodies}}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1d423f8b16..4530c71742 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -29,8 +29,8 @@ construction allows defining ``signatures''.
 {\recordkw} & ::= &
    {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\
   & & \\
-{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\
- & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term}
+{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\
+ & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\
 \end{tabular}
 \end{centerframe}
 \caption{Syntax for the definition of {\tt Record}}
@@ -213,7 +213,21 @@ Record point := { x : nat; y : nat }.
 Definition a := Build_point 5 3.
 \end{coq_example}
 
-The following syntax allows creating objects by using named fields. The
+\begin{figure}[t]
+\begin{centerframe}
+\begin{tabular}{lcl}
+{\term} & ++= &
+         \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\
+  & & \\
+{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\
+\end{tabular}
+\end{centerframe}
+\caption{Syntax for constructing elements of a \texttt{Record} using named fields}
+\label{fig:fieldsyntax}
+\end{figure}
+
+A syntax is available for creating objects by using named fields, as
+shown on Figure~\ref{fig:fieldsyntax}. The
 fields do not have to be in any particular order, nor do they have to be all
 present if the missing ones can be inferred or prompted for (see
 Section~\ref{Program}).
@@ -252,7 +266,7 @@ Eval compute in (
 Reset Initial.
 \end{coq_eval}
 
-\Rem An experimental syntax for projections based on a dot notation is
+\Rem A syntax for projections based on a dot notation is
 available. The command to activate it is
 \optindex{Printing Projections}
 \begin{quote}
@@ -267,7 +281,7 @@ available. The command to activate it is
  & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )}
 \end{tabular}
 \end{centerframe}
-\caption{Syntax of \texttt{Record} projections}
+\caption{Syntax for \texttt{Record} projections}
 \label{fig:projsyntax}
 \end{figure}
 
-- 
cgit v1.2.3