diff options
| -rw-r--r-- | proofs/goal.ml | 2 | ||||
| -rw-r--r-- | proofs/goal.mli | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 8 |
3 files changed, 4 insertions, 8 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 1542267e3..d68ab8c55 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -563,7 +563,7 @@ module V82 = struct let new_sigma = Evd.add Evd.empty evk new_evi in { Evd.it = build evk ; sigma = new_sigma } - (* Used by the typeclasses *) + (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = content sigma gl in let evi = Evarutil.nf_evar_info sigma evi in diff --git a/proofs/goal.mli b/proofs/goal.mli index e9d230659..9219d4a49 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -234,7 +234,7 @@ module V82 : sig (* Used for congruence closure *) val new_goal_with : Evd.evar_map -> goal -> Environ.named_context_val -> goal Evd.sigma - (* Used by the typeclasses *) + (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map (* Goal represented as a type, doesn't take into account section variables *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a363c6bbb..5babd03a8 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -685,12 +685,8 @@ let prim_refiner r sigma goal = ([gl], sigma) | Change_evars -> - (* spiwack: a priori [Change_evars] is now devoid of operational content. - The new proof engine keeping the evar_map up to date at all time. - As a compatibility mesure I leave the rule. - It is possible that my assumption is wrong and some uses of - [Change_evars] are not subsumed by the new engine. In which - case something has to be done here. (Feb. 2010) *) + (* Normalises evars in goals. Used by instantiate. *) + let (goal,sigma) = Goal.V82.nf_evar sigma goal in ([goal],sigma) (************************************************************************) |