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