From 506ef0526bd29e0f2f3e9f4c38261f67fe39fe4f Mon Sep 17 00:00:00 2001
From: bertot
Date: Tue, 3 Apr 2001 09:52:58 +0000
Subject: Make it possible to perform proofs by induction even on non-inductive
 types, as long as one provides the induction principle.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1522 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0dea04fac9..fd6a2a9729 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -960,8 +960,10 @@ let type_clenv_binding wc (c,t) lbind =
 
 let general_elim (c,lbindc) (elimc,lbindelimc) gl = 
   let (wc,kONT)  = startWalk gl in
-  let (_,_,t)    = reduce_to_ind (pf_env gl) (project gl) 
-		     (pf_type_of gl c)  in
+  let ct = pf_type_of gl c in
+  let t = try let (_,_,t)    = reduce_to_ind (pf_env gl) (project gl) ct in t 
+  with UserError _ -> ct
+  in
   let indclause  = make_clenv_binding wc (c,t) lbindc  in
   let elimt      = w_type_of wc elimc in
   let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
-- 
cgit v1.2.3