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

3 files changed, 3 insertions, 16 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 49e312aeb6..2de804aa13 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -139,7 +139,7 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Subtac_obligations.set_default_tactic (Tacinterp.glob_tactic t) ]
+| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Tacinterp.add_tacdef false [((dummy_loc, id_of_string "program_simpl"), true, t)] ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 0e9e042138..36a0e9c91a 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -599,14 +599,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
-(*     let evd,_ = consider_remaining_unif_problems env !isevars 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 = !isevars 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 *)
@@ -626,13 +620,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_tcc_evars evdref env kind c =
     pretype_gen evdref env ([],[]) kind c 
 
-(*     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 ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
       Evd.evars_of ev, t
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 46a8bd203c..bbdbe9a67a 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -195,7 +195,7 @@ let non_instanciated_map env evd evm =
 	     QuestionMark _ -> Evd.add evm key evi
 	   | _ ->
 	       debug 2 (str " and is an implicit");
-	       Pretype_errors.error_unsolvable_implicit loc env evm k)
+	       Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k)
     Evd.empty (Evarutil.non_instantiated evm)
     
 let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition