From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- proofs/goal.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'proofs/goal.ml') diff --git a/proofs/goal.ml b/proofs/goal.ml index dc1ac5dd..37ebce67 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -276,7 +276,7 @@ let check_typability env sigma c = let recheck_typability (what,id) env sigma t = try check_typability env sigma t - with _ -> + with e when Errors.noncritical e -> let s = match what with | None -> "the conclusion" | Some id -> "hypothesis "^(Names.string_of_id id) in @@ -474,7 +474,7 @@ module V82 = struct (* Old style hyps primitive *) let hyps evars gl = let evi = content evars gl in - evi.Evd.evar_hyps + Evd.evar_filtered_hyps evi (* Access to ".evar_concl" *) let concl evars gl = @@ -554,10 +554,16 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl new_hyps = + (* Used for congruence closure and change *) + let new_goal_with sigma gl extra_hyps = let evi = content sigma gl in - let new_evi = { evi with Evd.evar_hyps = new_hyps } in + let hyps = evi.Evd.evar_hyps in + let new_hyps = + List.fold_right Environ.push_named_context_val extra_hyps hyps in + let extra_filter = List.map (fun _ -> true) extra_hyps in + let new_filter = extra_filter @ evi.Evd.evar_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 evk = Evarutil.new_untyped_evar () in let new_sigma = Evd.add Evd.empty evk new_evi in -- cgit v1.2.3