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

12 files changed, 56 insertions, 64 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 49e312aeb..2de804aa1 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 0e9e04213..36a0e9c91 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 46a8bd203..bbdbe9a67 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
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
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 0a600bc64..236b6f30f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1331,13 +1331,13 @@ let solve_remaining_evars env initial_sigma evd c =
       | Evar (ev,args as k) when not (Evd.mem initial_sigma ev) ->
             let (loc,src) = evar_source ev !evdref in
 	    let sigma = evars_of !evdref in
+	    let evi = Evd.find sigma ev in
 	    (try 
-	      let evi = Evd.find sigma ev in
 	      let c = solvable_by_tactic env evi k src in
 	      evdref := Evd.evar_define ev c !evdref;
 	      c
 	    with Exit ->
-	      Pretype_errors.error_unsolvable_implicit loc env sigma src)
+	      Pretype_errors.error_unsolvable_implicit loc env sigma evi src)
       | _ -> map_constr proc_rec c      
   in
   proc_rec c
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index adfd1c3a3..3043a9239 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -166,25 +166,25 @@ Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => Morphism (m : a -> b) :=
 
 Definition respecting [ Setoid a R, Setoid b R' ] : Type := { morph : a -> b | respectful morph }.
 
-Obligations Tactic := try red ; program_simpl ; unfold equiv in * ; try tauto.
+Ltac program_simpl ::= try red ; default_program_simpl ; try tauto.
 
 Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
   Setoid ({ morph : a -> b | respectful morph })
   (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
   equiv_prf := Build_equivalence _ _ _ _ _.
 
-Next Obligation.
-Proof.
-  trans (y x0) ; eauto.
-  apply H.
-  refl.
-Qed.
+  Next Obligation.
+  Proof.
+    trans (y x0) ; eauto.
+    apply H.
+    refl.
+  Qed.
 
-Next Obligation.
-Proof.
-  sym ; apply H.
-  sym ; auto.
-Qed.
+  Next Obligation.
+  Proof.
+    sym ; apply H.
+    sym ; auto.
+  Qed.
 
 (** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
    some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
@@ -321,4 +321,8 @@ Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid :
   Setoid (a -> b)
   (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
   equiv_prf := Build_equivalence _ _ _ _ _.
-*)
\ No newline at end of file
+*)
+
+(** Reset the default Program tactic. *)
+
+Ltac program_simpl ::= default_program_simpl.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index d20b3df55..3b4d90a5c 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -106,18 +106,12 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
       else right
     else right.
 
-  Solve Obligations using unfold equiv ; program_simpl.
+  Solve Obligations using try red ; unfold equiv ; program_simpl.
 
   Next Obligation.
   Proof.
-    unfold equiv.
+    red.
     extensionality x.
     destruct x ; auto.
   Qed.
-  
-  Next Obligation.
-  Proof.
-    unfold equiv in *.
-    red ; intro ; subst.
-    discriminates.
-  Qed.
+
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index c3870e6bd..ad03de2f4 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -175,4 +175,6 @@ Ltac program_simplify :=
   simpl ; intros ; destruct_conjs ; simpl proj1_sig in * ; subst* ; try autoinjection ; try discriminates ;
     try (solve [ red ; intros ; destruct_conjs ; try autoinjection ; discriminates ]).
 
-Ltac program_simpl := program_simplify ; auto with *.
+Ltac default_program_simpl := program_simplify ; auto with *.
+
+Ltac program_simpl := default_program_simpl.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 784346b24..0b69c41e7 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -343,8 +343,25 @@ let explain_not_clean env ev t k =
   str "with a term using variable " ++ var ++ spc () ++
   str "which is not in its scope."
 
-let explain_unsolvable_implicit env k =
-  str "Cannot infer " ++ explain_hole_kind env k ++ str "."
+let pr_ne_context_of header footer env =
+  if Environ.rel_context env = empty_rel_context &
+    Environ.named_context env = empty_named_context  then footer
+  else pr_ne_context_of header env
+
+let explain_typeclass_resolution env evi k =
+  match k with
+      InternalHole | ImplicitArg _ ->
+	(match Typeclasses.class_of_constr evi.evar_concl with
+	  | Some c -> 
+	      let env = Evd.evar_env evi in
+		str"." ++ fnl () ++ str "Could not find an instance for " ++ 
+		  pr_lconstr_env env evi.evar_concl ++ 
+		  pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
+	  | None -> str ".")
+    | _ -> str "."
+
+let explain_unsolvable_implicit env evi k =
+  str "Cannot infer " ++ explain_hole_kind env k ++ explain_typeclass_resolution env evi k
 
 let explain_var_not_found env id =
   str "The variable" ++ spc () ++ pr_id id ++
@@ -432,7 +449,7 @@ let explain_pretype_error env err =
   | CantFindCaseType c -> explain_cant_find_case_type env c
   | OccurCheck (n,c) -> explain_occur_check env n c
   | NotClean (n,c,k) -> explain_not_clean env n c k
-  | UnsolvableImplicit k -> explain_unsolvable_implicit env k
+  | UnsolvableImplicit (evi,k) -> explain_unsolvable_implicit env evi k
   | VarNotFound id -> explain_var_not_found env id
   | UnexpectedType (actual,expect) -> explain_unexpected_type env actual expect
   | NotProduct c -> explain_not_product env c