diff options
| author | Hugo Herbelin | 2016-12-05 11:57:58 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-23 22:13:57 +0100 |
| commit | 45a411377244da33111cf5d7002df70de912bc64 (patch) | |
| tree | c01b496bbe54b7299fe8e7cafa279fcc55ddf05b /interp/constrexpr_ops.mli | |
| parent | 8f5d447769a41cd251701272a6ff71a7a20de658 (diff) | |
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.
Diffstat (limited to 'interp/constrexpr_ops.mli')
| -rw-r--r-- | interp/constrexpr_ops.mli | 3 |
1 files changed, 0 insertions, 3 deletions
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}*) |