| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
On a machine with only 1GB of memory (e.g. in a VM), the compiler might be
abruptly killed by a segfault. We were not getting any feedback in that
case, making it harder to debug.
|
| | | | | |
|
| |\ \ \ \
| | |/ /
| |/| |
| | | |
| | | | |
Conflicts:
lib/cSig.mli
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The Map interface of upcoming OCaml 4.03 includes a new union operator. In
order to make our homemade implementation of Maps compatible with OCaml
versions from 3.12 to 4.03, we define our own signatures for Maps.
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
|
| |\| | | |
|
| | | | | |
|
| | | | | |
|
| | |/ /
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The previous behavior was to include the interface of such a functor,
possibly leading to the creation of unexpected axioms, see bug report #3746.
In the case of non-functor module with restricted signature, we could
simply refer to the original objects (strengthening), but for a functor,
the inner objects have no existence yet. As said in the new error message,
a simple workaround is hence to first instantiate the functor, then include
the local instance:
Module LocalInstance := Funct(Args).
Include LocalInstance.
By the way, the mod_type_alg field is now filled more systematically,
cf new comments in declarations.mli. This way, we could use it to know
whether a module had been given a restricted signature (via ":"). Earlier,
some mod_type_alg were None in situations not handled by the extraction
(MEapply of module type).
Some code refactoring on the fly.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
typing. Had built the instance for substitution in the wrong context.
|
| |\| | |
|
| | | | |
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- prod_applist
- prod_applist_assum
- lambda_applist
- lambda_applist_assum
expect an instance matching the quantified context. They are now in
term.ml, with "list" being possibly "vect".
Names are a bit arbitrary. Better propositions are welcome. They are
put in term.ml in that reduction is after all not needed, because the
intent is not to do β or ι on the fly but rather to substitute a λΓ.c
or ∀Γ.c (seen as internalization of a Γ⊢c) into one step,
independently of the idea of reducing.
On the other side:
- beta_applist
- beta_appvect
are seen as optimizations of application doing reduction on the fly
only if possible. They are then kept as functions relevant for
reduction.ml.
|
| | | |
| | |
| | |
| | |
| | | |
to c71aa6b and 6ababf) so as to rely on generic functions rather than
re-doing the de Bruijn indices cooking locally.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Redefining adjust_subst_to_rel_context from instantiate_context who
was hidden in inductiveops.ml, renamed the latter into
subst_of_rel_context_instance and moving them to Vars. The new name
highlights that the input is an instance (as for applist) and the
output a substitution (as for substl). This is a clearer unified
interface, centralizing the difficult de-Bruijn job in one place. It
saves a couple of List.rev.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Related questions:
- What balance to find between precision and conciseness?
- What convention to follow for typesetting the different components
of the documentation is unclear?
New tentative type substl to emphasize that substitutions (for substl)
are represented the other way round compared to instances for
application (applist), though there are represented the same way
(i.e. most recent/dependent component on top) as instances of evars
(mkEvar).
Also removing unused subst*_named_decl functions (at least
substnl_named_decl is somehow non-sense).
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
next to each other, waiting for possible integration into a more
uniform API.
|
| | | | |
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
- Introduced an error: fold was counting in the wrong direction and I
did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
not correct.
Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
projections.
- lift accounting for the record missing in computing the subst from
fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.
This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.
Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.
|
| |\| |
| | |
| | |
| | | |
Did some manual merge in tactics/tactics.ml.
|
Matej Kosik
Guillaume Melquiond
Matthieu Sozeau
Maxime Dénès
Matthieu Sozeau
Pierre-Marie Pédrot
Pierre Letouzey
Hugo Herbelin
Gregory Malecha
Jacques-Henri Jourdan