From 4e98c439731c6e110430a6c5217274215bf403b6 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 12 May 2009 21:37:40 +0000
Subject: [PATCH] All weakly positive types but imbricated ones are now
 accepted (e.g. ordinals).

---
 .../components/ng_tactics/nCicElim.ml         | 43 +++++++++++--------
 helm/software/matita/tests/ng_elim.ma         | 11 +++++
 2 files changed, 37 insertions(+), 17 deletions(-)

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 54d8d5df6..1c041d1ee 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -70,23 +70,32 @@ let mk_elims (uri,_,_,_,obj) =
          let cargs_and_recursive_args =
           List.rev_map
            (function
-               name,NCic.Def _ -> assert false
-             | name,NCic.Decl (NCic.Const nref)
-             | name,NCic.Decl (NCic.Appl (NCic.Const nref::_))
-               when
-                let NReference.Ref (uri',_) = nref in
-                 NUri.eq uri uri'
-               ->
-                let name = mk_id name in
-                 name, Some (
-                 CicNotationPt.Appl
-                  (rec_name ::
-                   params @
-                   [p_name] @
-                   k_names @
-                   List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @
-                   [name]))
-             | name,_ -> mk_id name,None
+               _,NCic.Def _ -> assert false
+             | name,NCic.Decl ty ->
+                let context,ty = my_split_prods ~subst:[] [] (-1) ty in
+                 match ty with
+                  | NCic.Const nref
+                  | NCic.Appl (NCic.Const nref::_)
+                     when
+                      let NReference.Ref (uri',_) = nref in
+                       NUri.eq uri uri'
+                     ->
+                      let abs = List.rev_map (fun id,_ -> mk_id id) context in
+                      let name = mk_id name in
+                       name, Some (
+                       List.fold_right
+                        (fun id res ->
+                          CicNotationPt.Binder (`Lambda,(id,None),res))
+                        abs
+                        (CicNotationPt.Appl
+                         (rec_name ::
+                          params @
+                          [p_name] @
+                          k_names @
+                          List.map (fun _ -> CicNotationPt.Implicit)
+                           (List.tl args) @
+                          [CicNotationPt.Appl (name::abs)])))
+                  | _ -> mk_id name,None
            ) cargs in
          let cargs,recursive_args = List.split cargs_and_recursive_args in
          let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
diff --git a/helm/software/matita/tests/ng_elim.ma b/helm/software/matita/tests/ng_elim.ma
index c3b3d09bc..3ef667bdb 100644
--- a/helm/software/matita/tests/ng_elim.ma
+++ b/helm/software/matita/tests/ng_elim.ma
@@ -26,6 +26,17 @@ nlet rec nat_rec (Q: nat → Type) H_O H_S x_1 on x_1 : Q x_1 ≝
   | S x_2 ⇒ H_S x_2 (nat_rec Q H_O H_S x_2)
   ].
 
+
+ninductive ord: Type ≝
+   OO: ord
+ | OS: ord → ord
+ | OLim: (nat → ord) → ord.
+
+nlet rec ord_rect (Q_: (∀ (x_3: (ord)).Type)) H_OO H_OS H_OLim x_3 on x_3: (Q_ x_3) ≝
+ (match x_3 with [OO ⇒ (H_OO) | (OS x_4) ⇒ (H_OS x_4 (ord_rect Q_ H_OO H_OS H_OLim (x_4))) | (OLim x_6) ⇒ (H_OLim x_6 (λx_5.(ord_rect Q_ H_OO H_OS H_OLim (x_6 x_5))))]).
+
+
+
 naxiom P: nat → Prop.
 naxiom p: ∀m. P m.
 
-- 
2.39.2