From 87877b88aa97c4de2587b794eedced35d97ec8e4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 12 Dec 2008 12:11:54 +0000 Subject: [PATCH] added some hardcoded universes, needed to typecheck the librarya --- .../components/ng_disambiguation/nCicDisambiguate.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index a09c08599..0efb49bff 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -484,5 +484,16 @@ in NCicEnvironment.add_constraint true (mk_type 0) (mk_cprop 1); NCicEnvironment.add_constraint false (mk_cprop 0) (mk_type 0); NCicEnvironment.add_constraint false (mk_type 0) (mk_cprop 0); + + NCicEnvironment.add_constraint true (mk_type 1) (mk_type 2); + NCicEnvironment.add_constraint true (mk_cprop 1) (mk_cprop 2); + NCicEnvironment.add_constraint true (mk_cprop 1) (mk_type 2); + NCicEnvironment.add_constraint true (mk_type 1) (mk_cprop 2); + NCicEnvironment.add_constraint false (mk_cprop 1) (mk_type 1); + NCicEnvironment.add_constraint false (mk_type 1) (mk_cprop 1); + + NCicEnvironment.add_constraint false (mk_cprop 2) (mk_type 2); + NCicEnvironment.add_constraint false (mk_type 2) (mk_cprop 2); + ;; -- 2.39.2