diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 58 |
1 files changed, 24 insertions, 34 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 12d31e5f46..304b2dff84 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -60,19 +60,14 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) -let typeclass_resolvable = Evd.Store.field () - let dependent_init = - (* Goals are created with a store which marks them as unresolvable - for type classes. *) - let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in + let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in @@ -745,26 +740,28 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } -let mark_in_evm ~goal evd content = - let info = Evd.find evd content in - let info = +let mark_in_evm ~goal evd evars = + let evd = if goal then - { info with Evd.evar_source = match info.Evd.evar_source with - (* Two kinds for goal evars: - - GoalEvar (morally not dependent) - - VarInstance (morally dependent of some name). - This is a heuristic for naming these evars. *) - | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | - Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - else info - in - let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with - | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } - | Some () -> info + let mark evd content = + let info = Evd.find evd content in + let info = + { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + in Evd.add evd content info + in CList.fold_left mark evd evars + else evd in - Evd.add evd content info + let tcs = Evd.get_typeclass_evars evd in + let evset = Evar.Set.of_list evars in + Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset) let with_shelf tac = let open Proof in @@ -781,7 +778,7 @@ let with_shelf tac = let sigma = Evd.restore_future_goals sigma fgoals in (* Ensure we mark and return only unsolved goals *) let gls' = undefined_evars sigma (CList.rev_append gls' gls) in - let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let sigma = mark_in_evm ~goal:false sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -1035,7 +1032,7 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal evd content = + let mark_as_goals evd content = mark_in_evm ~goal:true evd content let advance = Evarutil.advance @@ -1043,9 +1040,7 @@ module Unsafe = struct let undefined = undefined let mark_as_unresolvable p gl = - { p with solution = mark_in_evm ~goal:false p.solution gl } - - let typeclass_resolvable = typeclass_resolvable + { p with solution = mark_in_evm ~goal:false p.solution [gl] } end @@ -1065,10 +1060,6 @@ let goal_nf_evar sigma gl = let sigma = Evd.add sigma gl evi in (gl, sigma) -let goal_extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra - let catchable_exception = function | Logic_monad.Exception _ -> false @@ -1093,7 +1084,6 @@ module Goal = struct let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl - let extra {sigma; self} = goal_extra sigma self let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; |