| Age | Commit message (Collapse) | Author |
|---|
|
|
|
as "forall x:nat*nat, x=x", which resulted in
"forall n n0 : nat, (n, n0) = (n, n0)" before commit
37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction
patterns * and ** ".
|
|
|
|
|
|
different places
|
|
- Add a tentative syntax for specifying universes: Type{"i"} and foo@{Type{"i"},Type{"j"}}.
These are always rigid.
- Use level-to-level substitutions where the more general level-to-universe substitutions
were previously used.
|
|
the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.
This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.
|
|
|
|
... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).
|
|
not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
|
|
|
|
|
|
correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.
|
|
required"
I tested the commit on the wrong branch...
This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
|
|
writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.
|
|
variant of it, accepting an additional integer.
|
|
|
|
|
|
parsing rule.
|
|
|
|
|
|
"foobar" constr(x1) ... constr(xn)
are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.
|
|
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
|
|
Example:
Inductive Pnat : Prop := O | S : Pnat -> Pnat.
Variable m n : Pnat.
Goal S (S O) = S O -> False.
intros H; injection H.
now deduces S O = O instead of failing with an error message.
|
|
|
|
Use Set Injection On Proof to enable the new behavior.
|
|
"coretactics.ml4" file.
|
|
|
|
corresponding Declare ML Module command. This changes essentially two
things:
1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.
2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.
|
|
|
|
|
|
fixing two opened bugs from HoTT/coq.
|
|
tactics.
|
|
(made push command with wrong local ref; leaving control to Matthieu
on new revert)
This reverts commit b797ba85b7b0f82d66af5629ccf6f75d90dda99a.
|
|
|
|
which compute an abstraction of the goal over a term or a pattern.
|
|
works in the presence of local definitions referring to x and
dependent in other hyps or concl.
|
|
|
|
Also removing trailing spaces.
|
|
evar_map
in tactics, avoiding useless and potentially costly merge's of constraints.
- Implement revert and generalize using the new tactics (not bound to syntax though,
as they are not backwards-compatible yet).
|
|
|
|
|
|
|
|
V82.tactic (tclEVARS _).
Again, performance is back to normal. Remove reintroduced try .. with _ -> in raw_enter's.
|
|
in the Evd of proofs (Evd.from_env).
- Allow to set the Store.t value of new evars, e.g. to set constraint evars as
unresolvable in rewrite.ml.
- Fix a HUGE performance problem in the processing of constraints, which was remerging
all the previous constraints with the ambient global universes at each new constraint addition.
Performance is now back to (or better than) normal.
|
|
minimization.
|
|
- Enforce that no u <= Prop/Set can be added for u introduced by the user in Evd.process_constraints.
(Needs to be enforced in the kernel as well, but that's the main entry point).
- Fix a test-suite script and remove a regression comment, it's just as before now.
|
|
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
|
|
presence of side-effects...
|
|
- Remove Universe Polymorphism flags everywhere.
- Properly infer, discharge template arities and fix substitution inside them
(kernel code to check for correctness).
- Fix tactics that were supposing universe polymorphic constants/inductives to
be parametric on that status. Required to make interp_constr* return the whole evar
universe context now.
- Fix the univ/level/instance hashconsing to respect the fact that marshalling doesn't preserve sharing,
sadly losing most of its benefits.
Short-term solution is to add hashes to these for faster comparison, longer term requires rewriting
all serialization code.
Conflicts:
kernel/univ.ml
tactics/tactics.ml
theories/Logic/EqdepFacts.v
|
