Work on dependent induction tactic and friends, finish the test-suite example

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

2 files changed, 3 insertions, 3 deletions

diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 28fc7e2906..cf9c90e17e 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -147,7 +147,9 @@ let new_instance ctx (instid, bk, cl) props =
 	  App (c, args) -> 
 	    let cl = Option.get (class_of_constr c) in
 	      cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
-	| _ -> assert false)
+	| _ -> 
+	    let cl = Option.get (class_of_constr c) in
+	      cl, ctx, [])
   in
   let env' = Classes.push_named_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index 36a0e9c91a..986825f25c 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -566,8 +566,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val 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 (evars_of evd) evd in
     let c' = nf_evar (evars_of evd) c' in
       isevars := evd;