From c2e3d63ca60b27abb5398ecbc8ebcaf8fb925206 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 18 Jan 2008 19:41:43 +0000 Subject: Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a wrapper around Ltac program_simpl ::= . !!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretyping.ml | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5b4e8e7cf..db492c026 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -695,14 +695,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in let c = pretype_gen evdref env lvar kind c in -(* let evd,_ = consider_remaining_unif_problems env !evdref in *) -(* let evd = nf_evar_defs evd in *) -(* let c = nf_evar (evars_of evd) c in *) -(* let evd = undefined_evars evd in *) -(* let evd = Typeclasses.resolve_typeclasses env sigma evd in *) -(* let c = nf_evar (evars_of evd) c in *) let evd,_ = consider_remaining_unif_problems env !evdref in - if fail_evar then check_evars env (Evd.evars_of evd) evd c; + if fail_evar then check_evars env Evd.empty evd c; evd, c (** Entry points of the high-level type synthesis algorithm *) @@ -721,13 +715,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c -(* let c = pretype_gen evdref env ([],[]) kind c in *) -(* evdref := nf_evar_defs !evdref; *) -(* let c = nf_evar (evars_of !evdref) c in *) -(* let evd = undefined_evars !evdref in *) -(* let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *) -(* evdref := evd; *) -(* nf_evar (evars_of evd) c *) let understand_tcc sigma env ?expected_type:exptyp c = let evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in -- cgit v1.2.3