From b353d48558a70c42e1ec2c779e3886abbf037cb2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 17:50:32 +0000 Subject: [PATCH] To test the translation. --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2