diff options
| -rw-r--r-- | API/API.mli | 5 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 1 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 3 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 4 |
5 files changed, 9 insertions, 5 deletions
diff --git a/API/API.mli b/API/API.mli index a0e77edd1..f7cc7ced3 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 diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b4d87dfdb..3fae20bcb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,6 @@ open Misctypes module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * EConstr.constr (************************************************************************) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 6e533f178..1bde4b44c 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -27,7 +27,6 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr type inference_hook = env -> evar_map -> evar -> evar_map * constr diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index cc81adb85..48fa2202e 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -13,11 +13,14 @@ open Evd open Evarutil open Evarsolve open Pp +open Glob_term (******************************************) (* Instantiation of existential variables *) (******************************************) +type glob_constr_ltac_closure = ltac_var_map * glob_constr + let depends_on_evar sigma evk _ (pbty,_,t1,t2) = let t1 = EConstr.of_constr t1 in let t2 = EConstr.of_constr t2 in diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b65ffb1be..5d6971596 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -7,9 +7,11 @@ (************************************************************************) open Evd -open Pretyping +open Glob_term (** Refinement of existential variables. *) +type glob_constr_ltac_closure = ltac_var_map * glob_constr + val w_refine : evar * evar_info -> glob_constr_ltac_closure -> evar_map -> evar_map |