diff options
| author | Maxime Dénès | 2016-09-15 16:51:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-01 13:24:30 +0200 |
| commit | ba0975d00f49684e33f763e171f9578a702eec85 (patch) | |
| tree | af2923930981470c9a64a038ca792c2f037d5dcc /API | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Move glob_constr_ltac_closure to evar_refiner.
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 |