Fix interface of resolve_typeclasses: onlyargs -> with_goals:

by default typeclass resolution is not launched on goal evars.

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

3 files changed, 76 insertions, 73 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9d259eee1..dbabf6160 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -171,8 +171,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   in
   let env' = push_rel_context ctx env in
   evars := Evarutil.nf_evar_map !evars;
-  evars := mark_resolvables !evars;
-  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
+  evars := resolve_typeclasses ~with_goals:false ~fail:true env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
     if abstract then
@@ -232,7 +231,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       (CHole (Pp.dummy_loc, None) :: props), rest
+		       (CHole (Pp.dummy_loc, Some Evd.GoalEvar) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
@@ -242,64 +241,72 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		Some (Inl (type_ctx_instance evars (push_rel_context ctx' env') 
 			     k.cl_props props subst))
       in	  
+      let term, termtype =
+	match subst with
+	| None -> let termtype = it_mkProd_or_LetIn cty ctx in
+	    None, termtype
+	| Some (Inl subst) ->
+	  let subst = List.fold_left2
+	    (fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
+	    [] subst (k.cl_props @ snd k.cl_context)
+	  in
+	  let app, ty_constr = instance_constructor k subst in
+	  let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
+	  let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
+	    Some term, termtype
+	| Some (Inr (def, subst)) ->
+	  let termtype = it_mkProd_or_LetIn cty ctx in
+	  let term = Termops.it_mkLambda_or_LetIn def ctx in
+	    Some term, termtype
+      in
+      let _ = 
 	evars := Evarutil.nf_evar_map !evars;
-	let term, termtype =
-	  match subst with
-	  | None -> let termtype = it_mkProd_or_LetIn cty ctx in
-	      None, termtype
-	  | Some (Inl subst) ->
-	      let subst = List.fold_left2
-		(fun subst' s (_, b, _) -> if b = None then s :: subst' else subst')
-		[] subst (k.cl_props @ snd k.cl_context)
+	evars := Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true
+          env !evars;
+	(* Try resolving fields that are typeclasses automatically. *)
+	evars := Typeclasses.resolve_typeclasses ~with_goals:true ~fail:false
+	  env !evars
+      in
+      let termtype = Evarutil.nf_evar !evars termtype in
+      let _ = (* Check that the type is free of evars now. *)
+	Evarutil.check_evars env Evd.empty !evars termtype
+      in
+      let term = Option.map (Evarutil.nf_evar !evars) term in
+      let evm = undefined_evars !evars in
+	if Evd.is_empty evm && term <> None then
+	  declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
+	else begin
+	  let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+	    if Flags.is_program_mode () then
+	      let hook vis gr =
+		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
+		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
 	      in
-	      let app, ty_constr = instance_constructor k subst in
-	      let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-	      let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
-		Some term, termtype
-	  | Some (Inr (def, subst)) ->
-	      let termtype = it_mkProd_or_LetIn cty ctx in
-	      let term = Termops.it_mkLambda_or_LetIn def ctx in
-		Some term, termtype
-	in
-	let termtype = Evarutil.nf_evar !evars termtype in
-	let term = Option.map (Evarutil.nf_evar !evars) term in
-	let evm = undefined_evars !evars in
-	  Evarutil.check_evars env Evd.empty !evars termtype;
-	  if Evd.is_empty evm && term <> None then
-	    declare_instance_constant k pri global imps ?hook id (Option.get term) termtype
-	  else begin
-	    evars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
-	    let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	      if Flags.is_program_mode () then
-		let hook vis gr =
-		  let cst = match gr with ConstRef kn -> kn | _ -> assert false in
-		    Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-		    Typeclasses.declare_instance pri (not global) (ConstRef cst)
-		in
-		let obls, constr, typ =
-		  match term with 
-		  | Some t -> 
-		      let obls, _, constr, typ = 
-			Obligations.eterm_obligations env id !evars 0 t termtype
-		      in obls, Some constr, typ
-		  | None -> [||], None, termtype
-		in
-		  ignore (Obligations.add_definition id ?term:constr
-			    typ ~kind:(Global,Instance) ~hook obls);
-		  id
-	      else
-		(Flags.silently 
-		   (fun () ->
-		      Lemmas.start_proof id kind termtype
-			(fun _ -> instance_hook k pri global imps ?hook);
-		      if term <> None then 
-			Pfedit.by (!refine_ref (evm, Option.get term))
-		      else if Flags.is_auto_intros () then
-			Pfedit.by (Refiner.tclDO len Tactics.intro);
-		      (match tac with Some tac -> Pfedit.by tac | None -> ())) ();
-		 Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
-		 id)
-	  end)
+	      let obls, constr, typ =
+		match term with 
+		| Some t -> 
+		  let obls, _, constr, typ = 
+		    Obligations.eterm_obligations env id !evars 0 t termtype
+		  in obls, Some constr, typ
+		| None -> [||], None, termtype
+	      in
+		ignore (Obligations.add_definition id ?term:constr
+			typ ~kind:(Global,Instance) ~hook obls);
+		id
+	    else
+	      (Flags.silently 
+	       (fun () ->
+		Lemmas.start_proof id kind termtype
+		(fun _ -> instance_hook k pri global imps ?hook);
+		if term <> None then 
+		  Pfedit.by (!refine_ref (evm, Option.get term))
+		else if Flags.is_auto_intros () then
+		  Pfedit.by (Refiner.tclDO len Tactics.intro);
+		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
+	       Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
+	       id)
+	end)
 	
 let named_of_rel_context l =
   let acc, ctx =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8bb875ffb..13139557a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -282,8 +282,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
 
   (* Instantiate evars and check all are resolved *)
   let evd = consider_remaining_unif_problems env_params !evdref in
-  let evd = Typeclasses.mark_resolvables evd in
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env_params evd in
   let sigma = evd in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in
   let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
@@ -768,7 +767,7 @@ let interp_recursive isfix fixl notations =
   (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots
 
 let check_recursive isfix ((env,rec_sign,evd),(fixnames,fixdefs,fixtypes),info) =
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
   List.iter (Option.iter (check_evars (push_named_context rec_sign env) Evd.empty evd)) fixdefs;
   List.iter (check_evars env Evd.empty evd) fixtypes;
   if not (List.mem None fixdefs) then begin
@@ -876,7 +875,7 @@ let do_program_recursive fixkind fixl ntns =
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instanciated *)
-  let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in
+  let evd = Typeclasses.resolve_typeclasses ~with_goals:false ~fail:true env evd in
     (* Solve remaining evars *)
   let rec collect_evars id def typ imps =
     (* Generalize by the recursive prototypes  *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a0bffd4fb..051eb3062 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -389,16 +389,13 @@ let explain_unsolvability = function
       strbrk " (several distinct possible instances found)"
 
 let explain_typeclass_resolution env evi k =
-  match k with
-  | GoalEvar | InternalHole | ImplicitArg _ ->
-      (match Typeclasses.class_of_constr evi.evar_concl with
-      | Some c ->
-	  let env = Evd.evar_env evi in
-	    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 -> mt())
-  | _ -> mt()
+  match Typeclasses.class_of_constr evi.evar_concl with
+  | Some c ->
+    let env = Evd.evar_env evi in
+      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 -> mt()
 
 let explain_unsolvable_implicit env evi k explain =
   str "Cannot infer " ++ explain_hole_kind env (Some evi) k ++