diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 23:34:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-25 13:37:03 +0100 |
| commit | c4d62e3686926c27b172636ca8b746814d13a462 (patch) | |
| tree | c7a627b0fb392e187fe0cd72ed39656d56b81504 /intf | |
| parent | a54579dd20e04ea919f8fa887e15dd82051fa297 (diff) | |
Moving type_uconstr to Pretyping.
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 b1dc174d4..0aa3b936c 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 |