aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* COMMENTS: Vernacexpr.extend_nameGravatar Matej Kosik2016-06-20
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge remote-tracking branch 'github/pr/194' into trunkGravatar Maxime Dénès2016-06-16
|\ \
| | * Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | * Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
| * | Adding an only printing flag to notations.Gravatar Pierre-Marie Pédrot2016-06-07
| * | Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
| |/
* / STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/
* Removing "rename" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "exact" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "intro" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing "double induction" from the tactic AST.Gravatar Pierre-Marie Pédrot2016-06-03
* Removing pointless field NPatVar. It does not make sense to have MetaGravatar Hugo Herbelin2016-06-02
* AlistNsep token now accepts an arbitrary separator.Gravatar Pierre-Marie Pédrot2016-05-10
* Simpler data structure for Arules token.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Removing the ad-hoc tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
* Expliciting the fact that the atomic tactic type is self-contained.Gravatar Pierre-Marie Pédrot2016-04-10
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\
* | Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* | Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* | Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | Allowing generalized rules in typed symbols.Gravatar Pierre-Marie Pédrot2016-03-19
* | Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
* | Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* | Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
* | Moving Ltac traces to Tacexpr and Tacinterp.Gravatar Pierre-Marie Pédrot2016-03-06
* | Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
* | Moving the "move" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "exists" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "symmetry" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "generalize dependent" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "clearbody" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "clear" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "cofix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* | Moving the "fix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 05:58:22 +0000