From b63f3d7db6e23746165f2a8501dfc3b52351530b Mon Sep 17 00:00:00 2001 From: msozeau Date: Thu, 17 Feb 2011 16:13:30 +0000 Subject: - Use transparency information all the way through unification and conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/evar_refiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/evar_refiner.ml') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fdd510831..36268de1e 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -30,7 +30,7 @@ let define_and_solve_constraints evk c evd = let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in fst (List.fold_left (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then Evarconv.evar_conv_x env evd pbty t1 t2 else p) (evd,true) + if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true) pbs) with e when Pretype_errors.precatchable_exception e -> error "Instance does not satisfy constraints." -- cgit v1.2.3