From 2c4dcfe11bdf6dae33566d353701965e41541ceb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Oct 2009 14:59:41 +0000
Subject: [PATCH] - 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)

---
 .../components/ng_kernel/nCicTypeChecker.ml   |  7 ++--
 helm/software/matita/tests/ng_bove.ma         | 33 +++++++++++++++++++
 2 files changed, 35 insertions(+), 5 deletions(-)
 create mode 100644 helm/software/matita/tests/ng_bove.ma

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 0b4b95eba..cd49f2cea 100644
--- 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
index 000000000..080bf7738
--- /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
-- 
2.39.2