diff options
| author | bertot | 2001-04-03 09:52:58 +0000 |
|---|---|---|
| committer | bertot | 2001-04-03 09:52:58 +0000 |
| commit | 506ef0526bd29e0f2f3e9f4c38261f67fe39fe4f (patch) | |
| tree | 02d738e88e19a4c0e26f1c04a94bb4a50fb714a8 | |
| parent | 056c60125b0052cebaa9a2a6e80005c2c7c85366 (diff) | |
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
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files 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 |