All weakly positive types but imbricated ones are now accepted

(e.g. ordinals).

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 54d8d5df62cfd27e2d9a28e862943fd5e1553c10..1c041d1eef8a1be882fbf2172cf42da7394f38c7 100644 (file)
--- 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 c3b3d09bca282ee37756171bbe539602924ce191..3ef667bdb2a53c62eb79b1bc95f31d0867fc596b 100644 (file)
--- 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.