diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 9 | ||||
| -rw-r--r-- | engine/evd.mli | 4 | ||||
| -rw-r--r-- | engine/proofview.ml | 14 | ||||
| -rw-r--r-- | engine/proofview.mli | 9 | ||||
| -rw-r--r-- | engine/univMinim.ml | 2 |
5 files changed, 24 insertions, 14 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 94868d9bdd..8e7d942c37 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -200,13 +200,14 @@ let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with in make_hyps filter (evar_context evi) -let evar_env evi = Global.env_of_context evi.evar_hyps +let evar_env env evi = + Environ.reset_with_named_context evi.evar_hyps env -let evar_filtered_env evi = match Filter.repr (evar_filter evi) with -| None -> evar_env evi +let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with +| None -> evar_env env evi | Some filter -> let rec make_env filter ctxt = match filter, ctxt with - | [], [] -> reset_context (Global.env ()) + | [], [] -> reset_context env | false :: filter, _ :: ctxt -> make_env filter ctxt | true :: filter, decl :: ctxt -> let env = make_env filter ctxt in diff --git a/engine/evd.mli b/engine/evd.mli index 7876e9a48f..8843adc853 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -125,8 +125,8 @@ val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body val evar_candidates : evar_info -> constr list option val evar_filter : evar_info -> Filter.t -val evar_env : evar_info -> env -val evar_filtered_env : evar_info -> env +val evar_env : env -> evar_info -> env +val evar_filtered_env : env -> evar_info -> env val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info diff --git a/engine/proofview.ml b/engine/proofview.ml index ed44372045..16be96454e 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1025,8 +1025,11 @@ module Unsafe = struct let undefined = undefined - let mark_as_unresolvable p gl = - { p with solution = mark_in_evm ~goal:false p.solution [gl] } + let mark_unresolvables evm evs = + mark_in_evm ~goal:false evm evs + + let mark_as_unresolvables p evs = + { p with solution = mark_in_evm ~goal:false p.solution evs } end @@ -1036,9 +1039,9 @@ let (>>=) = tclBIND (** {6 Goal-dependent tactics} *) -let goal_env evars gl = +let goal_env env evars gl = let evi = Evd.find evars gl in - Evd.evar_filtered_env evi + Evd.evar_filtered_env env evi let goal_nf_evar sigma gl = let evi = Evd.find sigma gl in @@ -1253,9 +1256,10 @@ module V82 = struct let of_tactic t gls = try + let env = Global.env () in let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in let name, poly = Names.Id.of_string "legacy_pe", false in - let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in + let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in { Evd.sigma = final.solution ; it = CList.map drop_state final.comb } with Logic_monad.TacticFailure e as src -> let (_, info) = CErrors.push src in diff --git a/engine/proofview.mli b/engine/proofview.mli index 8ec53ac78c..a92179ab5b 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -481,8 +481,13 @@ module Unsafe : sig and makes them unresolvable for type classes. *) val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map - (** Make an evar unresolvable for type classes. *) - val mark_as_unresolvable : proofview -> Evar.t -> proofview + (** Make some evars unresolvable for type classes. + We need two functions as some functions use the proofview and others + directly manipulate the undelying evar_map. + *) + val mark_unresolvables : Evd.evar_map -> Evar.t list -> Evd.evar_map + + val mark_as_unresolvables : proofview -> Evar.t list -> proofview (** [advance sigma g] returns [Some g'] if [g'] is undefined and is the current avatar of [g] (for instance [g] was changed by [clear] diff --git a/engine/univMinim.ml b/engine/univMinim.ml index 30fdd28997..fc0770cf75 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -276,7 +276,7 @@ let normalize_context_set ~lbound g ctx us algs weak = Constraint.partition (fun (l,d,r) -> d == Le && (Level.equal l lbound || Level.is_sprop l)) csts in let smallles = if get_set_minimization () - then Constraint.filter (fun (l,d,r) -> LSet.mem r ctx && not (Level.is_sprop l)) smallles + then Constraint.filter (fun (l,d,r) -> LMap.mem r us && not (Level.is_sprop l)) smallles else Constraint.empty in let csts, partition = |