aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\
| * Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\ \
| | * Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Gravatar Guillaume Melquiond2016-10-01
| |/
| * Merge remote-tracking branch 'github/pr/299' into v8.6Gravatar Maxime Dénès2016-09-30
| |\
| * | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| * | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| | * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| |/
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* | Moving Tacexpr to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
* | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
* | Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Support qualified identifiers in Show Match (bug #5050).Gravatar Guillaume Melquiond2016-08-27
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 23:49:14 +0000