aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Expand)AuthorAge
* Cleaning code in Pptactic.Gravatar Pierre-Marie Pédrot2014-09-02
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Simplification of Genarg unpackers.Gravatar Pierre-Marie Pédrot2014-08-29
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Improve consistency of whitespace (beautifier).Gravatar Xavier Clerc2014-08-21
* Space after [identity] coercion keywords (beautifier).Gravatar Xavier Clerc2014-08-21
* Avoid redundant spaces (beautifier).Gravatar Xavier Clerc2014-08-21
* Do not drop the locality qualifier (beautifier).Gravatar Xavier Clerc2014-08-21
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Refine patch for behavior of unify_to_subterm to allow backtracking onGravatar Matthieu Sozeau2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Preliminary re-installation of notation interpretation in beautifying mode.Gravatar Hugo Herbelin2014-08-05
* Fixing a few beautifying bugs.Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
* Fix typo in cf04daec997.Gravatar Arnaud Spiwack2014-08-01
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Removing dead code relative to or_metaid.Gravatar Pierre-Marie Pédrot2014-07-25
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
* Fix misleading pretty-printing of information for non-universe-polymorphicGravatar Matthieu Sozeau2014-07-24
* Missing space in pretty-printerGravatar Pierre-Marie Pédrot2014-07-21
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Locate: also display some information about module aliasingGravatar Pierre Letouzey2014-07-09
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Add toplevel commands to declare global universes and constraints.Gravatar Matthieu Sozeau2014-07-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 05:48:59 +0000