| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Ack-by: herbelin
|
|
Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output
|
|
|
|
These tactics now work correctly with multisuccess tactics by wrapping
the tactic argument in `once`.
Fixes #10965
|
|
extensionality
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: maximedenes
|
|
homotopy propositions and homotopy sets. Rename local variable R in test Nsatz, to avoid a name collision with the type of real numbers.
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
the Ltac-substituted environment
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
dune-compiled Coq
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
More precisely: The equivalent in #7288 (4dab4fc) to the former call
to ltac_interp_name_env was not done anymore when interpreting
uconstr's.
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This lets the checker verify that we didn't produce nonsense.
|
|
Reviewed-by: herbelin
|
|
|
|
This is the dual of #10344.
|
|
Fixes #9428. (Again.)
This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them.
Corrects a 8.9.1 → 8.10.0 regression.
(cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
|
|
Opening up a lambda should always lift the substitution attached to it.
|
|
AFAICT there is no reason to use interp_open_constr
I used Evd.from_ctx to keep passing evar maps around but maybe we
should be passing ustates instead?
|
|
i.e. you can do
~~~
make -f Makefile.dune world
make -C test-suite success
~~~
to make just the success tests, then modify Coq sources and retest
just the ones you want
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: hendriktews
Reviewed-by: herbelin
Ack-by: mattam82
|
|
|
|
|
|
database
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
sections
Reviewed-by: ppedrot
|
|
|
|
|
|
projections
Reviewed-by: fajb
|
|
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
intropattern entry in #10239)
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: fajb
|
|
Reviewed-by: mattam82
|
|
|
|
|
|
#10239).
The bug was introduced in #10239 which seems to have actually remained
half-done: "wit_intropattern" and "wit_simple_intropattern" did not
share the same representation of values (val_tag) but the code was
assuming (especially the code for "fresh") that this was shared.
We fix it by sharing the internal representation (`dyn` field in
Tacarg.make0) as suggested by @ppedrot in the discussion of #10239
(this allows also to simplify Taccoerce.is_intro_pattern).
|
|
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
Ack-by: vbgl
|
|
This helps extraction by not building sigT which can lower to Prop by
template polymorphism.
Bug #10757 can probably still be triggered by using module functors to
hide that we're using Prop from Program Fixpoint but that's probably
unfixable without fixing extraction vs template polymorphism in
general.
In passing we notice that Program doesn't know how to telescope SProp
arguments, we would need a bunch of variants of sigma types to deal
with it (or use Box?) so let's figure it out some other time.
We also reuse the universe instance to avoid generating a bunch of
short-lived universes in the universe polymorphic case.
|
|
The logic is implemented in OCaml. By induction over the terms,
guided by registered Coq terms in ZifyInst.v, it generates a rewriting
lemma. The rewriting is only performed if there is some progress. If
the rewriting fails (due to dependencies), a novel hypothesis is
generated.
This PR fixes #5155, fixes #8898, fixes #7886, fixes #10707, fixes #9848
ans fixes #10755.
The zify plugin is placed in the micromega directory.
(Though the reason is unclear, having it in a separate directory is
bad for efficiency.) efficiency impact.
There are also a few improvements of lia/lra that are piggybacked.
- more aggressive pruning of useless hypotheses
- slightly optimised conjunctive normal form
- applies exfalso if conclusion is not in Prop
- removal of Timeout in test-suite
|
|
Libraries are now handled like other modules.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
