| Age | Commit message (Collapse) | Author |
|---|
|
integrate to "rewrite"?) with the code of "replace".
Incidentally, "inversion" relies on dependent rewrite, with an
incompatibility introduced. Left-to-right rewriting is now done with
"eq_rec_r" while before it was done using "eq_rec" of "eq_sym". The
first one reduces to the second one but simpl is not anymore able to
reduce "eq_rec_r eq_refl". Hopefully cbn is able to do it (see
Zdigits).
|
|
|
|
Isolating a core tactic in replace, shareable to cutrewrite.
|
|
scheme, redundancies, possibility of chaining a tactic knowing the
name of introduced hypothesis, new proof engine).
|
|
|
|
- emphasizing the different kinds of patterns
- factorizing code of the non-naming intro-patterns
Still some questions:
- Should -> and <- apply to hypotheses or not (currently they apply to
hypotheses either when used in assert-style tactics or apply in, or
when the term to rewrite is a variable, in which case "subst" is
applied)?
- Should "subst" be used when the -> or <- rewrites an equation x=t
posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)?
- Should -> and <- be applicable in non assert-style if the lemma has
quantifications?
|
|
- made "apply" tactics of type Proofview.tactic, as well as other inner
functions about elim and assert
- used same hypothesis naming policy for intros and internal_cut (towards a
reorganization of intro patterns)
- "apply ... in H as pat" now supports any kind of introduction
pattern (doc not changed)
|
|
|
|
|
|
unsatisfiable constraint failures but give sensible error messages if
an occurrence was found and only typeclass resolution failed.
Fixes MathClasses.
|
|
|
|
|
|
|
|
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
|
|
|
|
|
|
(revealed by contribution PTSF).
|
|
|
|
|
|
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.
|
|
instead of the normalized one at the end of the proof. Fixes bug #3517.
|
|
|
|
|
|
when conversion in the goal failed.
|
|
test-suite
file HoTT_coq_089.v).
|
|
projections.
|
|
|
|
for typeclass errors.
|
|
output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v
Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
|
|
|
|
(AFAIU, it is the table of supported unicode characters which has to
be upgraded anyway.)
|
|
died" when coqtop or coqtopide.cmxs are in inconsistent state.
|
|
The lexer parses bullets only at the beginning of sentence. In
particular, the lexer recognizes sentences (this feature was
introduced for the translator and it is still used for the
beautifier). It recognized "." but not "...'. I added "..." followed
by space or eol as a terminator of sentences. I hope this is
compatible with the rest of the code dealing with end of
sentences.
Fixed also parse_to_dot which was not aware of "...".
Maybe there are similar things to do with coqide or PG?
|
|
change of printing format of forall (need more thinking).
|
|
projections and their expansion, allowing unfolding when it fails.
Cleanup code in reductionops.ml
|
|
its expansion if it could reduce (fixes bug #3480).
|
|
applications, solving part of bug #3503.
|
|
|
|
|
|
of the argument is smaller than the other one.
|
|
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
|
|
The levels added by the context are in general much fewer than the size of the
evarmap, so it is better to add them to the latter rather than doing it the
other way around.
|
|
a primitive application only if all parameters of [p] are implicit, falling
back to the internalization of the eta-expanded version otherwise. This makes
apply [p] succeed even if its record argument is not implicit, ensuring better
compatibility.
|
|
|
|
|
|
|
|
|
|
Fixes PTSF (though I have no idea what caused this bug to show up just yesterday).
|
|
In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
|
|
|
