Remove non-DFSG contentsupstream/8.4_gamma0+really8.4beta2+dfsg

12 files changed, 122 insertions, 97 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index 5ed335d0..f4d8b769 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -132,18 +132,29 @@ let rec chop_product n t =
       | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
       | _ -> None
 
-let evar_dependencies evm ev =
+let evars_of_evar_info evi =
+  Intset.union (Evarutil.evars_of_term evi.evar_concl)
+    (Intset.union
+	(match evi.evar_body with
+	| Evar_empty -> Intset.empty
+	| Evar_defined b -> Evarutil.evars_of_term b)
+	(Evarutil.evars_of_named_context (evar_filtered_context evi)))
+
+let evar_dependencies evm oev =
   let one_step deps =
     Intset.fold (fun ev s ->
       let evi = Evd.find evm ev in
-	Intset.union (Evarutil.evars_of_evar_info evi) s)
+      let deps' = evars_of_evar_info evi in
+	if Intset.mem oev deps' then
+	  raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev))
+	else Intset.union deps' s)
       deps deps
   in
   let rec aux deps =
     let deps' = one_step deps in
       if Intset.equal deps deps' then deps
       else aux deps'
-  in aux (Intset.singleton ev)
+  in aux (Intset.singleton oev)
       
 let move_after (id, ev, deps as obl) l = 
   let rec aux restdeps = function
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index ca1240e5..6a131d39 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -75,14 +75,14 @@ type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstra
 let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
   (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype),
   (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
-  Genarg.create_arg "subtac_gallina_loc"
+  Genarg.create_arg None "subtac_gallina_loc"
 
 type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
 
 let (wit_subtac_withtac : Genarg.tlevel withtac_argtype),
   (globwit_subtac_withtac : Genarg.glevel withtac_argtype),
   (rawwit_subtac_withtac : Genarg.rlevel withtac_argtype) =
-  Genarg.create_arg "subtac_withtac"
+  Genarg.create_arg None "subtac_withtac"
 
 VERNAC COMMAND EXTEND Subtac
 [ "Program" subtac_gallina_loc(g) ] -> [ Subtac.subtac g ]
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 710149ae..d626396f 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -82,11 +82,9 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
       Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps];
       hook loc gr)
 
-let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
-
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
-  print_subgoals ()
+  Vernacentries.print_subgoals ()
 
 let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
 
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 368d8bac..16d4e21e 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1845,7 +1845,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 			 refl_arg :: refl_args,
 			 pred slift,
 			 (Name id, b, t) :: argsign'))
-		   (env, 0, [], [], slift, []) args argsign
+		   (env, neqs, [], [], slift, []) args argsign
 	       in
 	       let eq = mk_JMeq
 		 (lift (nargeqs + slift) appt)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index c08dd16d..6b3fe718 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -52,7 +52,7 @@ let type_ctx_instance evars env ctx inst subst =
 	| None -> interp_casted_constr_evars evars env (List.hd l) t', List.tl l
 	| Some b -> substl subst b, l
       in
-       evars := resolve_typeclasses ~onlyargs:true ~fail:true env !evars;
+       evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
        let d = na, Some c', t' in
 	aux (c' :: subst, d :: instctx) l ctx
     | [] -> subst
@@ -107,9 +107,10 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
 	  Namegen.next_global_ident_away i (Termops.ids_of_context env)
   in
+  evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;  
+  let ctx = Evarutil.nf_rel_context_evar !evars ctx 
+  and ctx' = Evarutil.nf_rel_context_evar !evars ctx' in
   let env' = push_rel_context ctx env in
-  evars := Evarutil.nf_evar_map !evars;
-  evars := resolve_typeclasses ~onlyargs:false ~fail:true env !evars;
   let sigma =  !evars in
   let subst = List.map (Evarutil.nf_evar sigma) subst in
   let props =
@@ -157,6 +158,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 	    Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
   in	  
   evars := Evarutil.nf_evar_map !evars;
+  evars := resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~fail:true env !evars;
+  evars := resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:false env !evars;
   let term, termtype =
     match subst with
     | Inl subst ->
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 74f31a90..eb29bd04 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -27,6 +27,9 @@ open Subtac_errors
 open Eterm
 open Pp
 
+let app_opt env evars f t =
+  whd_betaiota !evars (app_opt f t)
+
 let pair_of_array a = (a.(0), a.(1))
 let make_name s = Name (id_of_string s)
 
@@ -80,7 +83,8 @@ module Coercion = struct
       | Type _, Prop Null -> Prop Null
       | _, Type _ -> s2
 
-  let hnf env isevars c = whd_betadeltaiota env ( !isevars) c
+  let hnf env isevars c = whd_betadeltaiota env isevars c
+  let hnf_nodelta env evars c = whd_betaiota evars c
 
   let lift_args n sign =
     let rec liftrec k = function
@@ -90,15 +94,16 @@ module Coercion = struct
       liftrec (List.length sign) sign
 
   let rec mu env isevars t =
-    let isevars = ref isevars in
     let rec aux v =
-      let v = hnf env isevars v in
+      let v = hnf env !isevars v in
       match disc_subset v with
 	  Some (u, p) ->
 	    let f, ct = aux u in
+	    let p = hnf env !isevars p in
 	      (Some (fun x ->
-		       app_opt f (mkApp ((delayed_force sig_).proj1,
-					 [| u; p; x |]))),
+		     app_opt env isevars 
+		     f (mkApp ((delayed_force sig_).proj1,
+			       [| u; p; x |]))),
 	       ct)
 	| None -> (None, v)
     in aux t
@@ -106,9 +111,8 @@ module Coercion = struct
   and coerce loc env isevars (x : Term.constr) (y : Term.constr)
       : (Term.constr -> Term.constr) option
       =
-    let x = nf_evar ( !isevars) x and y = nf_evar ( !isevars) y in
     let rec coerce_unify env x y =
-      let x = hnf env isevars x and y = hnf env isevars y in
+      let x = hnf env !isevars x and y = hnf env !isevars y in
 	try
 	  isevars := the_conv_x_leq env x y !isevars;
 	  None
@@ -167,7 +171,7 @@ module Coercion = struct
 	      let env' = push_rel (name', None, a') env in
 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 		(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
-	      let coec1 = app_opt c1 (mkRel 1) in
+	      let coec1 = app_opt env' isevars c1 (mkRel 1) in
 		(* env, x : a' |- c1[x] : lift 1 a *)
 	      let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
 		(* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
@@ -177,7 +181,7 @@ module Coercion = struct
 		    Some
 		      (fun f ->
 			mkLambda (name', a',
-				 app_opt c2
+				 app_opt env' isevars c2
 				   (mkApp (Term.lift 1 f, [| coec1 |])))))
 
 	  | App (c, l), App (c', l') ->
@@ -220,9 +224,9 @@ module Coercion = struct
 				     Some
 				       (fun x ->
 					  let x, y =
-					    app_opt c1 (mkApp (existS.proj1,
+					    app_opt env' isevars c1 (mkApp (existS.proj1,
 							       [| a; pb; x |])),
-					    app_opt c2 (mkApp (existS.proj2,
+					    app_opt env' isevars c2 (mkApp (existS.proj2,
 							       [| a; pb; x |]))
 					  in
 					    mkApp (existS.intro, [| a'; pb'; x ; y |]))
@@ -240,9 +244,9 @@ module Coercion = struct
 				     Some
 				       (fun x ->
 					  let x, y =
-					    app_opt c1 (mkApp (prod.proj1,
+					    app_opt env isevars c1 (mkApp (prod.proj1,
 							       [| a; b; x |])),
-					    app_opt c2 (mkApp (prod.proj2,
+					    app_opt env isevars c2 (mkApp (prod.proj2,
 							       [| a; b; x |]))
 					  in
 					    mkApp (prod.intro, [| a'; b'; x ; y |]))
@@ -276,7 +280,7 @@ module Coercion = struct
 	  Some (u, p) ->
 	    let c = coerce_unify env u y in
 	    let f x =
-	      app_opt c (mkApp ((delayed_force sig_).proj1,
+	      app_opt env isevars c (mkApp ((delayed_force sig_).proj1,
 				[| u; p; x |]))
 	    in Some f
 	| None ->
@@ -285,7 +289,7 @@ module Coercion = struct
 		  let c = coerce_unify env x u in
 		    Some
 		      (fun x ->
-			 let cx = app_opt c x in
+			 let cx = app_opt env isevars c x in
 			 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
 			 in
 			   (mkApp
@@ -300,7 +304,8 @@ module Coercion = struct
   let coerce_itf loc env isevars v t c1 =
     let evars = ref isevars in
     let coercion = coerce loc env evars t c1 in
-      !evars, Option.map (app_opt coercion) v
+    let t = Option.map (app_opt env evars coercion) v in
+      !evars, t
 
   (* Taken from pretyping/coercion.ml *)
 
@@ -354,34 +359,36 @@ module Coercion = struct
     with _ -> anomaly "apply_coercion"
 
   let inh_app_fun env isevars j =
-    let t = whd_betadeltaiota env ( isevars) j.uj_type in
+    let isevars = ref isevars in
+    let t = hnf env !isevars j.uj_type in
       match kind_of_term t with
-	| Prod (_,_,_) -> (isevars,j)
-	| Evar ev when not (is_defined_evar isevars ev) ->
-	    let (isevars',t) = define_evar_as_product isevars ev in
+	| Prod (_,_,_) -> (!isevars,j)
+	| Evar ev when not (is_defined_evar !isevars ev) ->
+	    let (isevars',t) = define_evar_as_product !isevars ev in
 	      (isevars',{ uj_val = j.uj_val; uj_type = t })
 	| _ ->
        	    (try
       	       let t,p =
-		 lookup_path_to_fun_from env ( isevars) j.uj_type in
-		 (isevars,apply_coercion env ( isevars) p j t)
+		 lookup_path_to_fun_from env !isevars j.uj_type in
+		 (!isevars,apply_coercion env !isevars p j t)
 	     with Not_found ->
 	       try
 		 let coercef, t = mu env isevars t in
-		   (isevars, { uj_val = app_opt coercef j.uj_val; uj_type = t })
+		 let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in
+		   (!isevars, res)
 	       with NoSubtacCoercion | NoCoercion ->
-		 (isevars,j))
+		 (!isevars,j))
 
   let inh_tosort_force loc env isevars j =
     try
       let t,p = lookup_path_to_sort_from env ( isevars) j.uj_type in
       let j1 = apply_coercion env ( isevars) p j t in
-	(isevars,type_judgment env (j_nf_evar ( isevars) j1))
+	(isevars, type_judgment env (j_nf_evar ( isevars) j1))
     with Not_found ->
       error_not_a_type_loc loc env ( isevars) j
 
   let inh_coerce_to_sort loc env isevars j =
-    let typ = whd_betadeltaiota env ( isevars) j.uj_type in
+    let typ = hnf env isevars j.uj_type in
       match kind_of_term typ with
 	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
 	| Evar ev when not (is_defined_evar isevars ev) ->
@@ -391,15 +398,19 @@ module Coercion = struct
 	    inh_tosort_force loc env isevars j
 
   let inh_coerce_to_base loc env isevars j =
-    let typ = whd_betadeltaiota env ( isevars) j.uj_type in
+    let isevars = ref isevars in
+    let typ = hnf env !isevars j.uj_type in
     let ct, typ' = mu env isevars typ in
-      isevars, { uj_val = app_opt ct j.uj_val;
-		 uj_type = typ' }
+    let res =
+      { uj_val = app_opt env isevars ct j.uj_val;
+	uj_type = typ' }
+    in !isevars, res
 
   let inh_coerce_to_prod loc env isevars t =
-    let typ = whd_betadeltaiota env ( isevars) (snd t) in
+    let isevars = ref isevars in
+    let typ = hnf env !isevars (snd t) in
     let _, typ' = mu env isevars typ in
-      isevars, (fst t, typ')
+      !isevars, (fst t, typ')
 
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
@@ -452,23 +463,23 @@ module Coercion = struct
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
   let inh_conv_coerce_to_gen rigidonly loc env evd cj ((n, t) as _tycon) =
     match n with
-	None ->
-	  let (evd', val') =
-	    try
-	      inh_conv_coerce_to_fail loc env evd rigidonly
-		(Some (nf_evar evd cj.uj_val))
-		(nf_evar evd cj.uj_type) (nf_evar evd t)
-	    with NoCoercion ->
-	      let sigma =  evd in
-		try
-		  coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
-		with NoSubtacCoercion ->
-		  error_actual_type_loc loc env sigma cj t
-	  in
-	  let val' = match val' with Some v -> v | None -> assert(false) in
-	    (evd',{ uj_val = val'; uj_type = t })
-      | Some (init, cur) ->
-	  (evd, cj)
+    | None ->
+      let cj = { cj with uj_type = hnf_nodelta env evd cj.uj_type } 
+      and t = hnf_nodelta env evd t in
+      let (evd', val') =
+	try
+	  inh_conv_coerce_to_fail loc env evd rigidonly
+	  (Some cj.uj_val) cj.uj_type t
+	with NoCoercion ->
+	(try
+	   coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
+	 with NoSubtacCoercion ->
+	   error_actual_type_loc loc env evd cj t)
+      in
+      let val' = match val' with Some v -> v | None -> assert(false) in
+	(evd',{ uj_val = val'; uj_type = t })
+    | Some (init, cur) ->
+      (evd, cj)
 
   let inh_conv_coerce_to = inh_conv_coerce_to_gen false
   let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index ecae6759..ced390aa 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -458,7 +458,7 @@ let interp_recursive fixkind l =
   (* Instantiate evars and check all are resolved *)
   let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
   let evd = Typeclasses.resolve_typeclasses
-    ~onlyargs:true ~split:true ~fail:false env_rec evd
+    ~filter:Typeclasses.no_goals ~split:true ~fail:false env_rec evd
   in
   let evd = Evarutil.nf_evar_map evd in
   let fixdefs = List.map (nf_evar evd) fixdefs in
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 64d9f72c..6a5878b3 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -445,12 +445,12 @@ let deps_remaining obls deps =
       else x :: acc)
     deps []
 
-let has_dependencies obls n =
-  let res = ref false in
+let dependencies obls n =
+  let res = ref Intset.empty in
     Array.iteri
       (fun i obl ->
 	if i <> n && Intset.mem n obl.obl_deps then
-	  res := true)
+	  res := Intset.add i !res)
       obls;
     !res
 
@@ -502,8 +502,9 @@ let rec solve_obligation prg num tac =
 		in
 		  match res with
 		  | Remain n when n > 0 ->
-		      if has_dependencies obls num then
-			ignore(auto_solve_obligations (Some prg.prg_name) None)
+		      let deps = dependencies obls num in
+			if deps <> Intset.empty then
+			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
 		  | _ -> ());
 	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
 		      Subtac_utils.my_print_constr (Global.env ()) obl.obl_type);
@@ -553,14 +554,18 @@ and solve_obligation_by_tac prg obls i tac =
 	| Util.Anomaly _ as e -> raise e
 	| e -> false
 
-and solve_prg_obligations prg tac =
+and solve_prg_obligations prg ?oblset tac =
   let obls, rem = prg.prg_obligations in
   let rem = ref rem in
   let obls' = Array.copy obls in
+  let p = match oblset with
+    | None -> (fun _ -> true)
+    | Some s -> (fun i -> Intset.mem i s)
+  in
   let _ =
     Array.iteri (fun i x ->
-		   if solve_obligation_by_tac prg obls' i tac then
-		     decr rem)
+		 if p i && solve_obligation_by_tac prg obls' i tac then
+		   decr rem)
       obls'
   in
     update_obls prg obls' !rem
@@ -582,9 +587,9 @@ and try_solve_obligation n prg tac =
 and try_solve_obligations n tac =
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
-and auto_solve_obligations n tac : progress =
+and auto_solve_obligations n ?oblset tac : progress =
   Flags.if_verbose msgnl (str "Solving obligations automatically...");
-  try solve_prg_obligations (get_prog_err n) tac with NoObligations _ -> Dependent
+  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent
 
 open Pp
 let show_obligations_of_prg ?(msg=true) prg =
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 7c0d1232..e56fa4f5 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -67,8 +67,8 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_map !isevars in
   let evd = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:false env unevd' in
+  let unevd' = Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations ~split:true ~fail:true env evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars ~split:true ~fail:false env unevd' in
   let evm =  unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index d5d427c7..9a4e1883 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -88,7 +88,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 
   (* coerce to tycon if any *)
   let inh_conv_coerce_to_tycon loc env evdref j = function
-    | None -> j_nf_evar !evdref j
+    | None -> j
     | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
 
   let push_rels vars env = List.fold_right push_rel vars env
@@ -323,7 +323,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
  	    else tycon
 	  in
 	    match ty with
-	    | Some (_, t) when Subtac_coercion.disc_subset t = None -> ty
+	    | Some (_, t) ->
+	      if Subtac_coercion.disc_subset (whd_betadeltaiota env !evdref t) = None then ty
+	      else None
 	    | _ -> None
 	in
 	let fj = pretype ftycon env evdref lvar f in
@@ -340,13 +342,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			Coercion.inh_conv_coerces_to loc env !evdref resty ty) tycon;
 		      let evd, (_, _, tycon) = split_tycon loc env !evdref tycon in
 		      evdref := evd;
-		      let hj = pretype (mk_tycon (nf_evar !evdref c1)) env evdref lvar c in
+		      let hj = pretype (mk_tycon c1) env evdref lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
-		      let typ' = nf_evar !evdref typ in
 			apply_rec env (n+1)
-			  { uj_val = nf_evar !evdref value;
-			    uj_type = nf_evar !evdref typ' }
-			  (Option.map (fun (abs, c) -> abs, nf_evar !evdref c) tycon) rest
+			{ uj_val = value;
+			  uj_type = typ }
+			  (Option.map (fun (abs, c) -> abs, c) tycon) rest
 
 		  | _ ->
 		      let hj = pretype empty_tycon env evdref lvar c in
@@ -354,9 +355,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env !evdref
 	      		  resj [hj]
 	in
-	let resj = j_nf_evar !evdref (apply_rec env 1 fj ftycon args) in
+	let resj = apply_rec env 1 fj ftycon args in
 	let resj =
-	  match kind_of_term resj.uj_val with
+	  match kind_of_term (whd_evar !evdref resj.uj_val) with
 	  | App (f,args) when isInd f or isConst f ->
 	      let sigma =  !evdref in
 	      let c = mkApp (f,Array.map (whd_evar sigma) args) in
@@ -508,10 +509,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
 	  let pred = nf_evar !evdref pred in
 	  let p = nf_evar !evdref p in
-	 (*   msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
 	  let f cs b =
 	    let n = rel_context_length cs.cs_args in
-	    let pi = lift n pred in (* liftn n 2 pred ? *)
+	    let pi = lift n pred in
 	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
 	    let csgn =
 	      if not !allow_anonymous_refs then
@@ -525,7 +525,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		cs.cs_args
 	    in
 	    let env_c = push_rels csgn env in
-(* 	      msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
 	    let bj = pretype (mk_tycon pi) env_c evdref lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
 	  let b1 = f cstrs.(0) b1 in
@@ -551,8 +550,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	    | CastConv (k,t) ->
 		let tj = pretype_type empty_valcon env evdref lvar t in
 		let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
-		  (* User Casts are for helping pretyping, experimentally not to be kept*)
-		  (* ... except for Correctness *)
 		let v = mkCast (cj.uj_val, k, tj.utj_val) in
 		  { uj_val = v; uj_type = tj.utj_val }
 	in
@@ -600,9 +597,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     in
       if resolve_classes then
 	(try 
-	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+	   evdref := Typeclasses.resolve_typeclasses ~filter:Subtac_utils.no_goals_or_obligations
 	     ~split:true ~fail:true env !evdref;
-	   evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+	   evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
 	     ~split:true ~fail:false env !evdref
 	 with e -> if fail_evar then raise e else ());
       evdref := consider_remaining_unif_problems env !evdref;
@@ -647,8 +644,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
   let understand_type sigma env c =
     snd (ise_pretype_gen true false true sigma env ([],[]) IsType c)
 
-  let understand_ltac expand_evar sigma env lvar kind c =
-    ise_pretype_gen expand_evar false true sigma env lvar kind c
+  let understand_ltac ?(resolve_classes=false) expand_evar sigma env lvar kind c =
+    ise_pretype_gen expand_evar false resolve_classes sigma env lvar kind c
 
   let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
     ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 28bbdd35..fbb44811 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -161,12 +161,11 @@ let print_args env args =
   Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
 
 let make_existential loc ?(opaque = Define true) env isevars c =
-  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
-  let (key, args) = destEvar evar in
-    (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
-		  print_args env args ++ str " for type: "++
-		  my_print_constr env c) with _ -> ());
-    evar
+  Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c
+
+let no_goals_or_obligations = function
+  | GoalEvar | QuestionMark _ -> false
+  | _ -> true
 
 let make_existential_expr loc env c =
   let key = Evarutil.new_untyped_evar () in
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index de96cc60..112b1795 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -82,6 +82,7 @@ val app_opt : ('a -> 'a) option -> 'a -> 'a
 val print_args : env -> constr array -> std_ppcmds
 val make_existential : loc -> ?opaque:obligation_definition_status ->
   env -> evar_map ref -> types -> constr
+val no_goals_or_obligations : Typeclasses.evar_filter
 val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 val string_of_hole_kind : hole_kind -> string
 val evars_of_term : evar_map -> evar_map -> constr -> evar_map