diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 385e100e2..0d9bde2ec 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -61,6 +61,7 @@ type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr type 'a delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } +type delayed_open_constr = constr delayed_open (************************************************************************) (* This concerns Cases *) |