Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.

The motivations are:

- To reflect the concrete syntax more closely.
- To factorize the different places where "contexts" are internalized:
  before this patch, there is a different treatment of `Definition f
  '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack
  to interpret `Definition f `pat := c : t`. With the patch, the fix
  to avoid seeing a variable named `pat` works for both `fun 'x =>
  ...` and `Definition f 'x := ...`.

The drawbacks are:

- Counterpart to reflecting the concrete syntax more closerly, there
  are more redundancies in the syntax. For instance, the case `CLetIn
  (na,b,t,c)` can appears also in the form `CProdN (CLocalDef
  (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`.
- Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.

7 files changed, 45 insertions, 40 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f7639d22d..693ab464d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1295,8 +1295,8 @@ let rec rebuild_return_type rt =
         CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
 	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
-				       Constrexpr.Default Decl_kinds.Explicit, rt],
+    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous],
+                                       Constrexpr.Default Decl_kinds.Explicit, rt)],
 			    CAst.make @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
@@ -1356,7 +1356,7 @@ let do_build_inductive
 			      acc)
 	  | None ->
 	     CAst.make @@ Constrexpr.CProdN
-	       ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+               ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
 		acc
 	       )
 	)
@@ -1423,7 +1423,7 @@ let do_build_inductive
 			    acc)
 	 | None ->
            CAst.make @@ Constrexpr.CProdN
-	   ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
+           ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)],
 	    acc
 	   )
       )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 58154d310..96e4a94d3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -591,11 +591,11 @@ and rebuild_nal aux bk bl' nal typ =
 	match nal,typ with 
 	  | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
 	  | [], _ -> rebuild_bl aux bl' typ
-	  | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } ->
+          | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } ->
 	     if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
 	     then
 	       let assum = CLocalAssum([na],bk,nal't) in
-	       let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in 
+               let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
 	       rebuild_nal
 		 (assum::aux)
 		 bk
@@ -604,7 +604,7 @@ and rebuild_nal aux bk bl' nal typ =
 		 (CAst.make @@ CProdN(new_rest,typ'))
 	     else
 	       let assum = CLocalAssum([na'],bk,nal't) in
-	       let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in 
+               let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in
 	       rebuild_nal
 		 (assum::aux)
 		 bk
@@ -731,10 +731,14 @@ let rec add_args id new_args = CAst.map (function
       end
   | CFix  _  | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.")
   | CProdN(nal,b1) ->
-        CProdN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal,
+        CProdN(List.map (function  CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
+                                 | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
+                                 | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
 	     add_args id new_args  b1)
   | CLambdaN(nal,b1) ->
-      CLambdaN(List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args  b2)) nal,
+      CLambdaN(List.map (function  CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2)
+                                 | CLocalDef (na,b1,t) -> CLocalDef (na,add_args id new_args b1,Option.map (add_args id new_args) t)
+                                 | CLocalPattern _ -> user_err (Pp.str "pattern with quote not allowed here.")) nal,
 	       add_args id new_args  b1)
   | CLetIn(na,b1,t,b2) ->
       CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2)
@@ -793,7 +797,7 @@ let rec chop_n_arrow n t =
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
     match t.CAst.v with
-      | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
+      | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, two results are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
 					     the remaining number of arrow to chop and [t'] we discard it and
@@ -805,7 +809,7 @@ let rec chop_n_arrow n t =
 	      let new_n =
 		let rec aux (n:int) = function
 		    [] -> n
-		| (nal,k,t'')::nal_ta' ->
+                | CLocalAssum(nal,k,t'')::nal_ta' ->
 		    let nal_l = List.length nal in
 		    if n >= nal_l
 		    then
@@ -813,9 +817,10 @@ let rec chop_n_arrow n t =
 		    else
 		      let new_t' = CAst.make @@
 			Constrexpr.CProdN(
-					((snd (List.chop n nal)),k,t'')::nal_ta',t')
+                                        CLocalAssum((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
 		      raise (Stop new_t')
+                | _ -> anomaly (Pp.str "Not enough products.")
 		in
 		aux n nal_ta'
 	    in
@@ -828,16 +833,13 @@ let rec chop_n_arrow n t =
 let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
   match b.CAst.v with
-    | Constrexpr.CLambdaN ((nal_ta), b') ->
+    | Constrexpr.CLambdaN (CLocalAssum(nal,k,ta) as d::rest, b') ->
 	begin
-	  let n =
-	    (List.fold_left (fun n (nal,_,_) ->
-			       n+List.length nal) 0 nal_ta )
-	  in
-	  let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in
-	  (List.map (fun (nal,k,ta) ->
-		       (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t''
+          let n = List.length nal in
+          let nal_tas,b'',t'' = get_args (CAst.make ?loc:b.CAst.loc @@ Constrexpr.CLambdaN (rest,b')) (chop_n_arrow n t) in
+          d :: nal_tas, b'',t''
 	end
+    | Constrexpr.CLambdaN ([], b) -> [],b,t
     | _ -> [],b,t
 
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index d792d4ff7..e68140828 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -115,10 +115,11 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
     match bl,ann with
         [([_],_,_)], None -> 1
       | _, Some x ->
-          let ids = List.map snd (List.flatten (List.map pi1 bl)) in
+          let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in
           (try List.index Names.Name.equal (snd x) ids
           with Not_found -> user_err Pp.(str "No such fix variable."))
       | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
+  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
   (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -126,6 +127,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) =
     user_err ~loc:aloc
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
+  let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in
   (id,CAst.make ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
@@ -160,7 +162,7 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc ?loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
+      CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
   | [] -> c
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e5ff47356..4f430b79e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -353,9 +353,10 @@ let string_of_genarg_arg (ArgumentType arg) =
     let rec strip_ty acc n ty =
       match ty.CAst.v with
           Constrexpr.CProdN(bll,a) ->
-            let nb =
-              List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
-            let bll = List.map (fun (x, _, y) -> x, y) bll in
+            let bll = List.map (function
+            | CLocalAssum (nal,_,t) -> nal,t
+            | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in
+            let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in
             if nb >= n then (List.rev (bll@acc)), a
             else strip_ty (bll@acc) (n-nb) a
         | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 9822da1c7..499154d50 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -835,9 +835,9 @@ let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
 let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t =  CAst.make ?loc @@
-   CLambdaN ([[loc, name], Default Explicit, ty], t)
+   CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
-   CProdN ([[Loc.tag Anonymous], Default Explicit, ty], t)
+   CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty)
 
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
@@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    | _, (_, Some ty) ->
     let rec force_type ty = CAst.(map (function
      | CProdN (abs, t) ->
-       n_binders := !n_binders +  List.length (List.flatten (List.map pi1 abs));
+       n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs));
        CProdN (abs, force_type t)
      | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
      | _ -> (mkCCast ty (mkCType None)).v)) ty in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 46403aef3..211cad3f5 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1023,10 +1023,10 @@ let rec format_local_binders h0 bl0 = match h0, bl0 with
   | _ -> []
   
 let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
-  | BFvar :: h, { v = CLambdaN ([[_, x], _, _], c) } ->
+  | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } ->
     let bs, c' = format_constr_expr h c in
     Bvar x :: bs, c'
-  | BFdecl _:: h, { v = CLambdaN ([lxs, _, t], c) } ->
+  | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } ->
     let bs, c' = format_constr_expr h c in
     Bdecl (List.map snd lxs, t) :: bs, c'
   | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } ->
@@ -1165,20 +1165,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder
  | [ ssrbvar(bv) ] ->
    [ let xloc, _ as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole xloc],mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ")" ] ->
    [ let xloc, _ as x = bvar_lname bv in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([[x],Default Explicit,mkCHole xloc],mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] ->
    [ let x = bvar_lname bv in
      (FwdPose, [BFdecl 1]),
-     CAst.make ~loc @@ CLambdaN ([[x], Default Explicit, t], mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) ]
  | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] ->
    [ let xs = List.map bvar_lname (bv :: bvs) in
      let n = List.length xs in
      (FwdPose, [BFdecl n]),
-     CAst.make ~loc @@ CLambdaN ([xs, Default Explicit, t], mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) ]
  | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] ->
    [ (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) ]
  | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] ->
@@ -1191,7 +1191,7 @@ GEXTEND Gram
   [  ["of" | "&"]; c = operconstr LEVEL "99" ->
      let loc = !@loc in
      (FwdPose, [BFvar]),
-     CAst.make ~loc @@ CLambdaN ([[Loc.tag ~loc Anonymous],Default Explicit,c],mkCHole (Some loc)) ]
+     CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ]
   ];
 END
 
@@ -1217,7 +1217,7 @@ let push_binders c2 bs =
   | ct -> loop false ct bs
 
 let rec fix_binders = let open CAst in function
-  | (_, { v = CLambdaN ([xs, _, t], _) } ) :: bs ->
+  | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs ->
       CLocalAssum (xs, Default Explicit, t) :: fix_binders bs
   | (_, { v = CLetIn (x, v, oty, _) } ) :: bs ->
     CLocalDef (x, v, oty) :: fix_binders bs
@@ -1325,13 +1325,13 @@ let intro_id_to_binder = List.map (function
   | IPatId id ->
       let xloc, _ as x = bvar_lname (mkCVar id) in
       (FwdPose, [BFvar]),
-        CAst.make @@ CLambdaN ([[x], Default Explicit, mkCHole xloc],
+        CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)],
           mkCHole None)
   | _ -> anomaly "non-id accepted as binder")
 
 let binder_to_intro_id = CAst.(List.map (function
-  | (FwdPose, [BFvar]), { v = CLambdaN ([ids,_,_],_) }
-  | (FwdPose, [BFdecl _]), { v = CLambdaN ([ids,_,_],_) } ->
+  | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) }
+  | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } ->
       List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids
   | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id]
   | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One]
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 7d0584a00..17409595a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -137,7 +137,7 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
 let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
 let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t = CAst.make ?loc @@
-   CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t)
+   CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t)
 let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((Loc.tag ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)