From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 8 Apr 2008 17:50:32 +0000 (+0000)
Subject: To test the translation.
X-Git-Tag: make_still_working~5395
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b353d48558a70c42e1ec2c779e3886abbf037cb2;p=helm.git

To test the translation.
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f1a99408a..2f43659e8 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -1064,7 +1064,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with