Use a lazy value for the message in FailError, so that it won't be

unnecessarily computed when the user won't see it (avoids the costly
nf_evar_defs in typeclass errors).
Add hook support for mutual definitions in Program.
Try to solve only the argument typeclasses when calling [refine].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 29 insertions, 20 deletions

diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 92ece7fe4..a54b3a86f 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -238,6 +238,7 @@ let reduce_fix =
 
 let declare_mutual_definition l =
   let len = List.length l in
+  let first = List.hd l in
   let fixdefs, fixtypes, fiximps = 
     list_split3
       (List.map (fun x -> 
@@ -245,11 +246,11 @@ let declare_mutual_definition l =
 	  (strip_lam_n len subs), snd (decompose_prod_n len typ), x.prg_implicits) l)
   in
 (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixkind = Option.get (List.hd l).prg_fixkind in
+  let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let boxed = true (* TODO *) in
-  let fixnames = (List.hd l).prg_deps in
+  let (local,boxed,kind) = first.prg_kind in
+  let fixnames = first.prg_deps in
   let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
@@ -264,9 +265,11 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
-    List.iter (Command.declare_interning_data ([],[])) (List.hd l).prg_notations;
+    List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
     Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
-    (match List.hd kns with ConstRef kn -> kn | _ -> assert false)
+    let gr = List.hd kns in
+    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
+      first.prg_hook local gr; kn
       
 let declare_obligation obl body =
   match obl.obl_status with
@@ -468,7 +471,7 @@ and solve_obligation_by_tac prg obls i tac =
 	    | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
 	    | Stdpp.Exc_located(_, Refiner.FailError (_, s))
 	    | Refiner.FailError (_, s) ->
-		user_err_loc (obl.obl_location, "solve_obligation", s)
+		user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
 	    | e -> false)
 
 and solve_prg_obligations prg tac = 
@@ -547,11 +550,11 @@ let add_definition n b t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 	
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) notations fixkind =
+let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
       (fun acc (n, b, t, imps, obls) ->
-	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind (fun _ _ -> ()) in
+	let prg = init_prog_info n b t deps (Some fixkind) notations obls imps kind hook in
 	  ProgMap.add n prg acc)
       !from_prg l
   in
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 50f189dde..2afcb1941 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -34,6 +34,7 @@ val add_mutual_definitions :
       (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list -> 
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
+  ?hook:Tacexpr.declaration_hook ->
   notations ->
   Command.fixpoint_kind -> unit
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index f1a57ffc1..c7e3895e0 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev =
     | None ->
 	raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
     | Some ev ->
-	let evi = Evd.find ( evd) ev in
+	let evi = Evd.find evd ev in
 	let loc, kind = Evd.evar_source ev evd in
 	  raise (Stdpp.Exc_located (loc, TypeClassError
 	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index b0239eeb4..8b3789c3b 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -335,10 +335,12 @@ let tclIDTAC_MESSAGE s gls =
 let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int * std_ppcmds
+exception FailError of int * std_ppcmds Lazy.t
 
 (* The Fail tactic *)
-let tclFAIL lvl s g = raise (FailError (lvl,s))
+let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
+
+let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =
   let (sigr,g) = unpackage gls in
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d6bd73ca4..9a587a965 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -134,7 +134,7 @@ val tclTHENLASTn    : tactic -> tactic array -> tactic
 val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 
 (* A special exception for levels for the Fail tactic *)
-exception FailError of int * Pp.std_ppcmds
+exception FailError of int * Pp.std_ppcmds Lazy.t
 
 (* Takes an exception and either raise it at the next
    level or do nothing. *)
@@ -151,6 +151,7 @@ val tclTHENTRY       : tactic -> tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> Pp.std_ppcmds -> tactic
+val tclFAIL_lazy     : int -> Pp.std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 8f548210b..9146d02c5 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -452,7 +452,6 @@ let resolve_all_evars debug m env p oevd do_split fail =
 	      if fail then 
 		(* Unable to satisfy the constraints. *)
 		let evm = if do_split then select_evars comp evd else evd in
-		let evm = Evarutil.nf_evars evm in
 		let _, ev = Evd.fold 
 		  (fun ev evi (b,acc) -> 
 		    (* focus on one instance if only one was searched for *)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index f1ecc4da9..ff644c143 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -372,7 +372,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
 
 let refine (evd,c) gl =
   let sigma = project gl in
-  let evd = Typeclasses.resolve_typeclasses (pf_env gl) evd in
+  let evd = Typeclasses.resolve_typeclasses ~onlyargs:true (pf_env gl) evd in
   let c = Evarutil.nf_evar evd c in
   let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
   (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 213dcc8d2..7260f1fd7 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -834,8 +834,9 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl =
 	  with 
 	  | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
 	  | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
-	      tclFAIL 0 (str"setoid rewrite failed: unable to satisfy the rewriting constraints." 
-			  ++ fnl () ++ Himsg.explain_typeclass_error env e) gl)
+	      Refiner.tclFAIL_lazy 0 
+		(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints." 
+			++ fnl () ++ Himsg.explain_typeclass_error env e)) gl)
     | Some None -> 
 	tclFAIL 0 (str"setoid rewrite failed: no progress made") gl
     | None -> raise Not_found
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c21a4c080..0942fde83 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1918,7 +1918,7 @@ and eval_with_fail ist is_lazy goal tac =
   with
     | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) 
     | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
-	raise (Eval_fail s)
+	raise (Eval_fail (Lazy.force s))
     | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
     | Stdpp.Exc_located(s,FailError (lvl,s')) ->
 	raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ab7120b8b..2b69d7233 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -59,6 +59,7 @@ let tclINFO          = Refiner.tclINFO
 let tclCOMPLETE      = Refiner.tclCOMPLETE
 let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE
 let tclFAIL          = Refiner.tclFAIL
+let tclFAIL_lazy     = Refiner.tclFAIL_lazy
 let tclDO            = Refiner.tclDO
 let tclPROGRESS      = Refiner.tclPROGRESS
 let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index fe6dd2d64..762c7dc76 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -53,6 +53,7 @@ val tclINFO          : tactic -> tactic
 val tclCOMPLETE      : tactic -> tactic
 val tclAT_LEAST_ONCE : tactic -> tactic
 val tclFAIL          : int -> std_ppcmds -> tactic
+val tclFAIL_lazy     : int -> std_ppcmds Lazy.t -> tactic
 val tclDO            : int -> tactic -> tactic
 val tclPROGRESS      : tactic -> tactic
 val tclWEAK_PROGRESS : tactic -> tactic
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 4250040ec..f9a336430 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -85,7 +85,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
   | RecursionSchemeError e -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
-  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when s <> mt () ->
+  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
       explain_exn_default_aux anomaly_string report_fn exc
   | Proof_type.LtacLocated (s,exc) ->
       hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
@@ -108,7 +108,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
                Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
       hov 0 (str "Error: Tactic failure" ++ 
-                (if s <> mt() then str ":" ++ s else mt ()) ++
+                (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
                 if i=0 then str "." else str " (level " ++ int i ++ str").")
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4e5eded8e..e8a8dcb7c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -525,7 +525,7 @@ let pr_constraints printenv env evm =
       pr_evar_defs evm
       
 let explain_unsatisfiable_constraints env evd constr =
-  let evm =  evd in
+  let evm = Evarutil.nf_evars evd in
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++