Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside

inductive and Program defs. Fix eterm bug when generating obligations
and remove optimization of let-in removal which prevents factorization 
of proofs/"asserts" in Program.


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

4 files changed, 6 insertions, 8 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 9bfb33ea77..c2309c833e 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -46,7 +46,7 @@ let subst_evar_constr evs n t =
 	  let rec aux hyps args acc =
 	     match hyps, args with
 		 ((_, None, _) :: tlh), (c :: tla) -> 
-		   aux tlh tla ((map_constr_with_binders succfix substrec (depth, fixrels) c) :: acc)
+		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
 	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
 		   aux tlh tla acc
 	       | [], [] -> acc
@@ -93,8 +93,8 @@ let etype_of_evar evs hyps concl =
 	let trans' = Idset.union trans trans' in
 	  (match copt with
 	      Some c -> 
-		if noccurn 1 rest then lift (-1) rest, s', trans'
-		else
+(* 		if noccurn 1 rest then lift (-1) rest, s', trans' *)
+(* 		else *)
 		  let c', s'', trans'' = subst_evar_constr evs n c in
 		  let c' = subst_vars acc 0 c' in
 		    mkNamedProd_or_LetIn (id, Some c', t'') rest, 
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
index 5f10ac1d38..bf854abb3f 100644
--- a/contrib/subtac/eterm.mli
+++ b/contrib/subtac/eterm.mli
@@ -16,8 +16,6 @@ open Util
 
 val mkMetas : int -> constr list
 
-(* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *)
-
 (* env, id, evars, number of
    function prototypes to try to clear from evars contexts, object and type *)
 val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index a393e2c9b5..130d6858ba 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -562,8 +562,8 @@ let next_obligation n =
   let prg = get_prog_err n in
   let obls, rem = prg.prg_obligations in
   let i = 
-    array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = [])
-      obls
+    try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
+    with Not_found -> anomaly "Could not find a solvable obligation."
   in solve_obligation prg i
       			
 let default_tactic () = !default_tactic
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 78ee2f5cea..f65e3f786d 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -73,7 +73,7 @@ let interp env isevars c tycon =
   let _ = isevars := Evarutil.nf_evar_defs !isevars in
   let evd,_ = consider_remaining_unif_problems env !isevars in
 (*   let unevd = undefined_evars evd in *)
-  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env evd in
+  let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in
   let evm = evars_of unevd' in
     isevars := unevd';
     nf_evar evm j.uj_val, nf_evar evm j.uj_type