| Age | Commit message (Collapse) | Author |
|---|
|
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
|
|
|
|
It seems there were 4 copies of the same function in the code base.
|
|
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
|
|
|
This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
|
|
This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c.
|
|
This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62.
|
|
This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
|
|
fix au revert [||]
|
|
"|]"" because this commit triggers a
Error: Files proofs/proofs.cma(Miscprint)
and /usr/local/lib/ocaml/compiler-libs/ocamlcommon.cma(Lexer)
make inconsistent assumptions over interface Lexer
Adding two extra spaces systematically instead.
This reverts commit 72be1f6beafafc3edd30df673fbb6c7e88f8fac7.
|
|
exist as a keyword by inserting a space inbetween.
|
|
|
|
|
|
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
|
|
|
|
|
(the action is "clear").
Added subst_intropattern which was missing since the introduction of
ApplyOn intro patterns.
Still to do: make "intros _ ?id" working without interferences when
"id" is precisely the internal name used for hypotheses to discard.
|
|
"pat/term" for "apply term on current_hyp as pat".
|
|
- 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?
|
|
NB: new file miscprint.ml deserves to be part of printing.cma,
but should be part of proofs.cma for the moment, due to use in logic.ml
|
