aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Expand)Author
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-27COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...Matej Kosik
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-04Quick fix to #4595 (making notations containing "ltac:" unused for printing).Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-01Add command 'Set foo Append "bar"' for appending to an option (bug #5109).Guillaume Melquiond
2016-09-30Merge remote-tracking branch 'github/pr/299' into v8.6Maxime Dénès
2016-09-29Fix bug #4798: compat notations should not modify the parser.Pierre-Marie Pédrot
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-09-15Moving Tacexpr to ltac/ folder.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-09-08Making Vernacexpr independent from Tacexpr.Pierre-Marie Pédrot
2016-08-27Support qualified identifiers in Show Match (bug #5050).Guillaume Melquiond
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-20COMMENTS: Vernacexpr.extend_nameMatej Kosik
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-17par: like all: but in parallelEnrico Tassi
2016-06-16Extend Hint Mode to handle the no-head-evar caseMatthieu Sozeau
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-16Merge remote-tracking branch 'github/pr/194' into trunkMaxime Dénès
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-06-07Adding an only printing flag to notations.Pierre-Marie Pédrot
2016-06-07Removing the use to Egramcoq.recover_constr_grammar.Pierre-Marie Pédrot
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-02Removing pointless field NPatVar. It does not make sense to have MetaHugo Herbelin
2016-05-10AlistNsep token now accepts an arbitrary separator.Pierre-Marie Pédrot
2016-05-10Simpler data structure for Arules token.Pierre-Marie Pédrot
2016-05-10Removing the Entry module now that rules need not be marshalled.Pierre-Marie Pédrot
2016-04-27Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Hugo Herbelin
2016-04-27In the short term, stronger invariant on the syntax of TacAssert, whatHugo Herbelin
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-10Expliciting the fact that the atomic tactic type is self-contained.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:02:58 +0000