diff options
| author | Pierre-Marie Pédrot | 2016-03-25 15:14:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-25 15:14:30 +0100 |
| commit | d0a2ea9c4a68c33753c75cc80e4b255366c6352b (patch) | |
| tree | 6cc1208059a78d1f85042467542d35871120f831 /intf | |
| parent | a54579dd20e04ea919f8fa887e15dd82051fa297 (diff) | |
| parent | e8114ee084cae195eb7615293cec0e28dcc0a3d8 (diff) | |
Moving back some tactics not essentially related to Ltac into the tactics/ folder.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index b1dc174d4b..0aa3b936ca 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -122,7 +122,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type 'a delayed_open = +type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open |