- too strict check on left parameters of constructors in guarded by constructors removed
- the cases Fixpont and CoFixpoint in guarded by constructors are useless code in the
new kernel since:
o recursive/corecursive objects are now closed terms
o we do not allow (yet?) to pass co-recursive functions around
o we do check that the arguments of the application of a fix/cofix do not
contain the function we are checking for GBC
matitadep: we now handle the inline of an uri, we removed the -exclude option
matitaInit: we removed the -drop option (now handled automatically)
transcript: we removed the baseuri generation
CoRN-Procedural: the mma files and the depends file are now available
Procedural: some comments added in the generated script
tests/fguidi.ma: we removed the dependence from legacy/coq.ma
ApplyTransformation: new function procedural_text_of_cic_term
for use in matitaScript (still disabled)
a) update with upstream version
b) new: implemented semantic analyzer from untyped to typed AST for
an imperative structured function-less C compiler
c) all URIs removed from .ma files
lambda-delta: we added the support for position indexes in global references
we added a pretty printer for the intermediate language
librarian : utime stamps now appear only in debug mode
cicUtil : we added a context to is_sober to check for consistancy
of RELS (not implemented yet)
doubleTypeInference: the inferred name of an anonymous lambda must be the name
of the expected prod :)
acic2Procedural : we added a consistancy check that was missing
librarian: retrieval of buildable files speeded up a lot
Procedural: some bug fixes
termContentPres.ml: syntax of let-in construction fixed
LAMBDA-TYPES: some improvements in the Makefile
New feature/bug fixed (hopefully): it is now possible to use fixed (term)
variables in fold bodies.
The notation for exists is now fully working as expected.
Notation for existential partially fixed: it is now possible to write
\exists a,b,c:T.P
(possibly omitting the type).
In any case, however, the type is got rid of during parsing.
A very nice experiment using notation: we define the notation for natural
language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).
Exists is no longer an ad-hoc notation hard-coded in the parser.
It was so becauses it was previously impossible to declare a notation that
changed the level of its subterms.
CProp hierarchy fixed:
- CProp universes are not swept away
- CProp i : Type j (where i < j, used to be a fresh j)
- new kernel universe inconsistency error message improved
- pp function for universes constraints for new kernel
Formal topology example fixed to eploit left parameters to reduce the universe
height and solve universe inconsistency
simplified coercDb implementation with additional info about the position of
the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a
coercion and ? are implicits or saturations generated to apply the coercion to
x.
New case in unification, when there is a triangular pullback and the
coerced is not flexible an unfolding of the composed coercion is attempted.
this helps in the case:
C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z
where C = C1 composed C2 but X is rigid abd conversion fails cause
x != ? and the heads are different... unfolding C helps
- Procedural: bug fix in rendering the application: we must handle the
arguments that are inferrable but do not occur in the goal
- LAMBDA-TYPES: bug fix in Makefile: MAS was not computed correctly
projects / helm.git / log