]> matita.cs.unibo.it Git - helm.git/commit
huge commit regarding universes:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Sep 2009 10:01:28 +0000 (10:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 21 Sep 2009 10:01:28 +0000 (10:01 +0000)
commit8b1a49bbee9eea86eb74c040defe701370ca5893
treee2219bed9cadb585f030b3a4ab0c37463cea41e2
parent41068e795dcb5fd0e2f87d755d7f12b3cbb0f79b
huge commit regarding universes:
- only Type[foo] can be declare with a strict (<) constraint among other
  Type[bar]
- CProp[foo] is automatically available for Type[foo]
- The CProp hierarchy can be collapsed (hopefully in a consistent way)
  to both Prop OR Type:
  - You cannot eliminate CProp to build a Type like for Prop/Type
  - You cannot eliminate Prop to build a CProp, like for Prop/Type
- Peculiarity: CProp[i] has type Type[i+1], since CProp[i+1] is only >=
  of CProp[i] to allow collapsing them (while < whould be violated).

New function to delift a type w.r.t. a term list, to potentially build a
dependent type, used in lambda_intro and Letin expected type propagation.
34 files changed:
helm/software/components/content_pres/cicNotationParser.ml
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/ng_disambiguation/nCicDisambiguate.ml
helm/software/components/ng_kernel/check.ml
helm/software/components/ng_kernel/nCic.ml
helm/software/components/ng_kernel/nCic2OCic.ml
helm/software/components/ng_kernel/nCicEnvironment.ml
helm/software/components/ng_kernel/nCicEnvironment.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_kernel/nCicPp.ml
helm/software/components/ng_kernel/nCicReduction.ml
helm/software/components/ng_kernel/nCicTypeChecker.ml
helm/software/components/ng_kernel/oCic2NCic.ml
helm/software/components/ng_paramodulation/paramod.ml
helm/software/components/ng_refiner/.depend.opt
helm/software/components/ng_refiner/check.ml
helm/software/components/ng_refiner/nCicRefiner.ml
helm/software/components/ng_refiner/nCicUnification.ml
helm/software/components/ng_refiner/nCicUnification.mli
helm/software/components/ng_tactics/.depend
helm/software/components/ng_tactics/.depend.opt
helm/software/components/ng_tactics/Makefile
helm/software/components/ng_tactics/nCicElim.ml
helm/software/components/ng_tactics/nCicElim.mli
helm/software/components/ng_tactics/nTacStatus.ml
helm/software/components/ng_tactics/nTactics.ml
helm/software/matita/contribs/formal_topology/overlap/depends
helm/software/matita/nlibrary/logic/connectives.ma
helm/software/matita/nlibrary/logic/pts.ma
helm/software/matita/nlibrary/sets/partitions.ma
helm/software/matita/nlibrary/sets/sets.ma