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.

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 =