diff options
Diffstat (limited to 'proofs/goal.ml')
| -rw-r--r-- | proofs/goal.ml | 25 |
1 files changed, 7 insertions, 18 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index ba7e458f..c14c0a8a 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -48,7 +48,7 @@ module V82 = struct (* Access to ".evar_concl" *) let concl evars gl = let evi = Evd.find evars gl in - EConstr.of_constr evi.Evd.evar_concl + evi.Evd.evar_concl (* Access to ".evar_extra" *) let extra evars gl = @@ -61,7 +61,6 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) - let concl = EConstr.Unsafe.to_constr concl in let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; @@ -86,7 +85,7 @@ module V82 = struct if not (Evarutil.occur_evar_upto sigma evk c) then () else Pretype_errors.error_occur_check Environ.empty_env sigma evk c in - Evd.define evk (EConstr.Unsafe.to_constr c) sigma + Evd.define evk c sigma (* Instantiates a goal with an open term, using name of goal for evk' *) let partial_solution_to sigma evk evk' c = @@ -100,7 +99,9 @@ module V82 = struct let same_goal evars1 gl1 evars2 gl2 = let evi1 = Evd.find evars1 gl1 in let evi2 = Evd.find evars2 gl2 in - Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl && + let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in + let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in + Constr.equal c1 c2 && Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps let weak_progress glss gls = @@ -117,20 +118,6 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl extra_hyps = - let evi = Evd.find sigma gl in - let hyps = evi.Evd.evar_hyps in - let new_hyps = - List.fold_right Environ.push_named_context_val extra_hyps hyps in - let filter = evi.Evd.evar_filter in - let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in - let new_evi = - { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in - let new_evi = Typeclasses.mark_unresolvable new_evi in - let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = sigma; } - (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = Evd.find sigma gl in @@ -156,3 +143,5 @@ module V82 = struct ) ~init:(concl sigma gl) env end + +module Set = Set.Make(struct type t = goal let compare = Evar.compare end) |