aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Add a "Hint Mode ref (+ | -)*" hint for setting a global modeGravatar Matthieu Sozeau2014-09-15
* Checking typability of evar instances. Using ";" to separate bindingsGravatar Hugo Herbelin2014-09-13
* Add syntax [id]: to apply tactic to goal named id.Gravatar Hugo Herbelin2014-09-12
* Parsing evar instances.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* VernacExtend does not dispatch on type anymore.Gravatar Pierre-Marie Pédrot2014-09-10
* Removing dead code relative to the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Factorize the parsing rules of [Record] and the other kind of type definitions.Gravatar Arnaud Spiwack2014-09-04
* Remove [Infer] option of records.Gravatar Arnaud Spiwack2014-09-04
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* 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
* Fixing bug #3493.Gravatar Pierre-Marie Pédrot2014-08-27
* Removing a unused legacy parsing rule.Gravatar Pierre-Marie Pédrot2014-08-24
* 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
* 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
* Fixing parsing of bullets after a "...".Gravatar 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
* 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
* Small refactoring: use [uconstr] instead of [constr] when relevant in grammar...Gravatar Arnaud Spiwack2014-08-05
* Properly declare uconstr as an argument for TACTIC EXTEND.Gravatar Arnaud Spiwack2014-08-05
* 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
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* 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
* Fixing #3390 (mismatch simple_tactic/tactic0 leading to segfault).Gravatar Hugo Herbelin2014-06-21
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Gravatar Matthieu Sozeau2014-06-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 00:28:15 +0000