| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
Of course such proofs cannot be processed asynchronously
|
| | |
|
| |
|
|
|
|
|
|
| |
This is done by adding a fourth type of loadpath, the ones that are
neither implicit nor root, for the subdirectories of a -Q root.
Note: this means that scanning for available directories is no longer done
on the fly for -Q, but once and for all, as with -R.
|
| |
|
|
|
|
| |
optimized. Now "Import Arith ZArith" imports only once the libraries
reexported by both Arith and ZArith. (No side effect can be inserted
here, so that this looks compatible).
|
| | |
|
| |
|
|
| |
Follow-up on Matthieu's d030ce0721.
|
| |
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
|
|
|
| |
This reverts commit 6d5b56d971506dfadcfc824bfbb09dc21718e42b but does not put
back in place the Requires inside modules that were found in the std lib.
Conflicts:
kernel/safe_typing.ml
|
| | |
|
| |
|
|
| |
This is a follow-up on Pierre's 5d80a385.
|
| |
|
|
|
|
| |
into monomorphic constants, which was still using the de Bruijn encoding
Bug revealed by discharging of hidden internal monomorphic definition in
otherwise polymorphic developments. Makes coqchk work on Hurkens again.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After this commit, module_type_body is a particular case of module_type.
For a [module_type_body], the implementation field [mod_expr] is
supposed to be always [Abstract]. This is verified by coqchk, even
if this isn't so crucial, since [mod_expr] is never read in the case
of a module type.
Concretely, this amounts to the following rewrite on field names
for module_type_body:
- typ_expr --> mod_type
- typ_expr_alg --> mod_type_alg
- typ_* --> mod_*
and adding two new fields to mtb:
- mod_expr (always containing Abstract)
- mod_retroknowledge (always containing [])
This refactoring should be completely transparent for the user.
Pros: code sharing, for instance subst_modtype = subst_module.
Cons: a runtime invariant (mod_expr = Abstract) which isn't
enforced by typing. I tried a polymorphic typing of mod_expr,
to share field names while not having mtb = mb, but the OCaml
typechecker isn't clever enough with polymorphic mutual fixpoints,
and reject code sharing (e.g. between subst_modtype and subst_module).
In the future (with ocaml>=4), some GADT could maybe help here,
but for now the current solution seems good enough.
|
| |
|
|
|
|
| |
Removing unused argument and fixing bug #3899, now warning when a record
cannot be made primitive in Set Primitive Projections mode because it
has no projection or at least one undefinable projection.
|
| |
|
|
|
|
|
| |
Fixes #3379 and part of #3363. Also avoids fragile code propagating required
libraries when closing an interactive module.
Had to fix a few occurrences in std lib.
|
| |
|
|
|
| |
API to let one forge a frozen state out of another frozen state
plus some frozen bits
|
| |
|
|
|
|
| |
In this way one can make surgery on the system states, like
checking if two frozen states have the same environment (i.e.
no running "abstract" in between)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
| |
|
|
|
| |
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)
Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
|
| | |
|
| |
|
|
|
|
|
| |
inductive types (i.e., ones declared with an explicit anonymous Type
at the conclusion of their arity). With this change one can force
inductives to live in higher universes even in the non-fully universe
polymorphic case (e.g. bug #3821).
|
| |
|
|
| |
This is a continuation of the previous patch.
|
| | |
|
| |
|
|
|
|
|
|
| |
These dependencies between files can be used by UIs to guide compilation
and reloading of files.
FileDependency (Some "/foo.v", "/bar.v") means foo depends on bar.
FileDependency (None, "/bar.v") means the current file depends on bar.
|
| | |
|
| |
|
|
|
| |
This generalizes the BuildVi flag and lets one choose which
opaque proofs are done and which not.
|
| |
|
|
|
| |
Now the seff contains it directly, no need to force the future
or to hope that it is a Direct opaque proof.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).
With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
1) directly (before the constant is discharged)
2) indirectly, via an int, that is mapped by the opaque table to
the proof term.
This is now consistent in batch/interactive mode
This is step 0 to make an interactive coqtop able to dump a .vo/.vi
|
| |
|
|
|
|
|
| |
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(but deactivated still).
Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.
Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:
Declare Equivalent Keys f g.
This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.
For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.
INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
|
| |
|
|
| |
projections with their eta-expanded constant form.
|
| | |
|
| |
|
|
| |
implicits do not allow to parse as an application and cleanup code.
|
| |
|
|
|
|
|
|
| |
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
|
| | |
|
| |
|
|
| |
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
|
| |
|
|
|
|
| |
Local Ltac definitions do not register their name in the nametab anymore,
thus elegantly solving the bug. The tactic body remains accessible from
the tactic engine, but the name is rendered meaningless to the userside.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
now done entirely using declare_mind, which declares the associated
constants for primitive records. This avoids a hack related to
elimination schemes and ensures that the forward references to constants
in the mutual inductive entry are properly declared just after the
inductive. This also clarifies (and simplifies) the code of term_typing
for constants which does not have to deal with building
or checking projections anymore.
Also fix printing of universes showing the de Bruijn encoding in a few places.
|
| |
|
|
|
|
|
|
|
|
|
| |
Now kernel/indtypes builds the corresponding terms (has to be trusted)
while translate_constant just binds a constant name to the
already entered projection body, avoiding the dubious "check"
of user given terms. "case" Pattern-matching on primitive records is
now disallowed, and the default scheme is implemented using
projections and eta (all elimination tactics now use projections
as well). Elaborate "let (x, y) := p in t" using let bindings
for the projections of p too.
|
| | |
|
| | |
|
| | |
|
| | |
|
Enrico Tassi
Guillaume Melquiond
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Matthieu Sozeau
Pierre Letouzey
Matthieu Sozeau
Carst Tankink
Arnaud Spiwack
Jason Gross