From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 2 Apr 2009 10:50:23 +0000 (+0000)
Subject: added analyse_indty
X-Git-Tag: make_still_working~4124
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9f1f0cb1ae2665a495db930f1561e381e64f5137;p=helm.git

added analyse_indty
---

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 87be3279f..49daed849 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -531,19 +531,26 @@ let intro_tac name =
    (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
 ;;
 
-let case status goal =
- let _,ctx,_ = get_goal status goal in
- let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in
- let ref =
-  match whd status (`Ctx ctx) ty with
-     _,_,NCic.Const ref
-   | _,_,NCic.Appl (NCic.Const ref :: _) -> ref
+let analyse_indty status ty = 
+ let ref, args =
+  match whd status (`Term ty) ty with
+   | _,_,NCic.Const ref -> ref, []
+   | _,_,NCic.Appl (NCic.Const ref :: args) -> ref, args
    | _,_,_ -> fail (lazy ("not an inductive type")) in
- let _,_,tl,_,i = NCicEnvironment.get_checked_indtys ref in
+ let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
  let _,_,_,cl = List.nth tl i in
  let consno = List.length cl in
+ let left, right = HExtlib.split_nth lno args in
+ ref, consno, left, right
+;;
+
+let case status goal =
+ let _,ctx,_ = get_goal status goal in
+ let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in
+ let ref, consno, left, right = analyse_indty status ty in
  let t =
-  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,HExtlib.mk_list (NCic.Implicit `Term) consno)
+  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
+    HExtlib.mk_list (NCic.Implicit `Term) consno)
  in
  let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in
  instantiate status goal t