aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/miscprint.ml
Commit message (Collapse)AuthorAge
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-06-16
|
* Revert "Fixing printing of pat%constr."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 6f3dc50176fff8b731dcdaf47194f0e3ff21db0c.
* Revert "Protect printing of intro-patterns from collision when "[|" or "|]""Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit e9abd74adc486c1c1793754fdf83a33fe7b1b34c.
* Revert "Revert "Protect printing of intro-patterns from collision when "[|" or"Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit fd8669f9f2e37607f5eba56ba25e267711876e62.
* Revert "Fixing extra space in front of terminal in printing vernac."Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit 834885cb8cbc4d6924a63b898c7a5a32cfd0211c.
* Fixing extra space in front of terminal in printing vernac.Gravatar Hugo Herbelin2016-04-27
| | | | fix au revert [||]
* Revert "Protect printing of intro-patterns from collision when "[|" orGravatar Hugo Herbelin2016-04-27
| | | | | | | | | | | | "|]"" 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.
* Protect printing of intro-patterns from collision when "[|" or "|]"Gravatar Hugo Herbelin2016-04-27
| | | | exist as a keyword by inserting a space inbetween.
* Fixing printing of pat%constr.Gravatar Hugo Herbelin2016-04-27
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | 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.
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (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.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - 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?
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 20:54:15 +0000