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.

2 files changed, 22 insertions, 20 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