| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Print and Extraction commands may pierce opacity: if the
task producing the proof term is not finished, we wait for
its completion.
In -quick mode no worker is going to process a task, since tasks
are simply stored to disk (and resumed later in -vio2vo mode).
This commit avoids coqc waits forever for a task in order to
Print/Extract the corresponding term. Bug reported privately
by Alec Faithfull.
|
|
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
|
|
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
|
|
|
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
|
|
|
variables and definitions in sections is unsupported.
|
|
|
|
|
|
|
|
|
|
Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
|
|
This fixes a TODO in map_constr_expr_with_binders, a bug in
is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
|
|
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
|
|
constant and arguments _separately_.
|
|
|
|
Also ensure we stay compatible with 8.4: progress could now be made
simply because of beta redexes in the goal.
|
|
|
|
The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
|
|
The rewrite tactic was causing an evar leak because of the use of the
Evd.remove primitive. This function did not modify the future goals of
the evarmap to remove the considered evar and thus maintained dangling
evars in there, causing the anomaly.
|
|
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.
|
|
|
|
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
|
|
|
During an extraction, a few tables are maintained to cache
intermediate results. Due to modules, the kernel_name index
for these caching tables aren't enough. For instance, in
bug #3923, a constant is first transparent (from inside the
module) then opaque (when seen from the signature). The previous
protections were actually obsolete (tests via visible_con), we
now checks that the constant_body is still the same.
|
|
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
|
|
|
|
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
|
|
|
|
|
|
|
|
|
|
|
|
Marking it as experimental.
|
|
|
|
|
|
based on a suggestion of Guillaume M. (done like this in ssreflect).
This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
|
|
Do not substitute rigid variables during minimization, keeping
their equality constraints instead.
|
|
|
|
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
|
|
|
|
|
|
|
|
|
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.
|
|
The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.
|
|
parameters of an inductive type.
|
|
|
