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

4 files changed, 8 insertions, 20 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1f256b3bd..e8d79703a 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1004,7 +1004,8 @@ let check_evars env initial_sigma evd c =
           assert (Evd.mem sigma evk);
 	  if not (Evd.mem initial_sigma evk) then
             let (loc,k) = evar_source evk evd in
-	    error_unsolvable_implicit loc env sigma k
+	    let evi = nf_evar_info sigma (Evd.find sigma evk) in
+	    error_unsolvable_implicit loc env sigma evi k
       | _ -> iter_constr proc_rec c
   in proc_rec c
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ad4e06a55..420e0ef9b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -25,7 +25,7 @@ type pretype_error =
   (* Unification *)
   | OccurCheck of existential_key * constr
   | NotClean of existential_key * constr * Evd.hole_kind
-  | UnsolvableImplicit of Evd.hole_kind
+  | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind
   | CannotUnify of constr * constr
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -152,8 +152,8 @@ let error_not_clean env sigma ev c (loc,k) =
   raise_with_loc loc
     (PretypeError (env_ise sigma env,  NotClean (ev,c,k)))
 
-let error_unsolvable_implicit loc env sigma e =
-  raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e))
+let error_unsolvable_implicit loc env sigma evi e =
+  raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e)))
 
 let error_cannot_unify env sigma (m,n) =
   raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 3a2a2f7f4..c949462c1 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -27,7 +27,7 @@ type pretype_error =
   (* Unification *)
   | OccurCheck of existential_key * constr
   | NotClean of existential_key * constr * Evd.hole_kind
-  | UnsolvableImplicit of Evd.hole_kind
+  | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind
   | CannotUnify of constr * constr
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
@@ -93,7 +93,7 @@ val error_not_clean :
   env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
 
 val error_unsolvable_implicit :
-  loc -> env -> Evd.evar_map -> Evd.hole_kind -> 'b
+  loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind -> 'b
 
 val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
 
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