To test the translation.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index f1a99408ab80764685a0486deb696eb070f98ec9..2f43659e823d5a547d6603bcc56150b619227b8d 100644 (file)
--- 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