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.
---
 interp/constrexpr_ops.mli | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'interp/constrexpr_ops.mli')

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 :
-- 
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.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'interp/constrexpr_ops.mli')

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}*)
 
-- 
cgit v1.2.3