diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli index a0e77edd12..f7cc7ced36 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4008,7 +4008,6 @@ sig } type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr val understand_ltac : inference_flags -> Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> @@ -4387,8 +4386,10 @@ end module Evar_refiner : sig + type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr + val w_refine : Evar.t * Evd.evar_info -> - Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map + glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map end |