From 2b9f73c7e86ac718c0ce4c47d6a24ffc2d01499d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 30 Jan 2008 04:21:51 +0000
Subject: 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
---
 contrib/subtac/subtac_classes.ml     | 4 +++-
 contrib/subtac/subtac_pretyping_F.ml | 2 --
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'contrib')

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;
-- 
cgit v1.2.3