added analyse_indty

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 87be3279f18ade3f1f49ad8bbebb443e94251d9c..49daed849e0fab1f9cbfaf7413b04b6d3f7f8ac8 100644 (file)
--- 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