- Bug fixed: some assert failure were just failures (when processing terms

  that do not satisfy the IRS condition).
- New test ng_bove.ma added to test the Bove-Capretta method (in CProp)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 0b4b95eba3dd2bc58d92b12056c47589791abf43..cd49f2cea93332c7de1eb428292240225d4df6b2 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1052,10 +1052,7 @@ and is_really_smaller
     is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
  | C.Appl (he::_) ->
     is_really_smaller r_uri r_len ~subst ~metasenv k he
- | C.Rel _ 
- | C.Const (Ref.Ref (_,Ref.Con _)) -> false
- | C.Appl [] 
- | C.Const (Ref.Ref (_,Ref.Fix _)) -> assert false
+ | C.Appl [] | C.Implicit _ -> assert false
  | C.Meta _ -> true 
  | C.Match (Ref.Ref (_,Ref.Ind (isinductive,_,_)),_,term,pl) ->
     (match term with
@@ -1073,7 +1070,7 @@ and is_really_smaller
              is_really_smaller r_uri r_len ~subst ~metasenv k e)
            pl dcl
     | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl)
- | _ -> assert false
+ | _ -> false
 
 and returns_a_coinductive ~subst context ty =
   match R.whd ~subst context ty with

diff --git a/helm/software/matita/tests/ng_bove.ma b/helm/software/matita/tests/ng_bove.ma
new file mode 100644 (file)
index 0000000..080bf77
--- /dev/null
+++ b/helm/software/matita/tests/ng_bove.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+
+include "nat/minus.ma".
+
+ninductive D: nat → Prop ≝
+   D0: D O
+ | Dn: ∀n. D (n - 2) → D n.
+ 
+naxiom dow: ∀n,m.∀p: D n. n = S m → False.
+naxiom destr: ∀n. O = S n → False.
+
+nlet rec f (n:nat) (p:D n) on p : nat ≝
+ match n return λm. n=m → nat with
+  [ O ⇒ λ_.O
+  | S m ⇒ λH. f (n - 2) ?] (refl_eq ? n).
+ ncases p in H
+  [ #K; ncases (destr ? K)
+  | #n0; #p; #H; nassumption ]
+nqed.
\ No newline at end of file