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

1 files changed, 1 insertions, 14 deletions

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