aboutsummaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
AgeCommit message (Expand)Author
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-05-15Merge v8.5 into trunkHugo Herbelin
2015-05-11Adding a test to check whether two tactic notations conflict.Pierre-Marie Pédrot
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-16Fixing bug #4190.Pierre-Marie Pédrot
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-24Revert "Useless check when loading notations through import."Pierre-Marie Pédrot
2015-02-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-11Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-10Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-04Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-03Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Enrico Tassi
2015-02-03Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-01-21Embedding the index of the ML tactic entry in the Tacexpr AST.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-16Fixing CAMLP4 compilation.Pierre-Marie Pédrot
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-15Failing on unbound notation variable in notation level modifiersHugo Herbelin
2014-10-17Now printing "now a keyword" only in verbose mode.Hugo Herbelin
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-09-03Additional entry tactic_arg in Print Grammar tactic.Pierre-Marie Pédrot
2014-08-31Getting rid of atomic tactics in Tacenv.Pierre-Marie Pédrot
2014-08-18Moving the TacExtend node from atomic to plain tactics.Pierre-Marie Pédrot
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-06-30Useless keeping of dirpath in tactic aliases.Pierre-Marie Pédrot
2014-05-13Fix the behaviour of ML tactic notations w.r.t. Imports by making themPierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-01Useless check when loading notations through import.Pierre-Marie Pédrot
2014-02-25Fixing printing of only_parsing notations.Pierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Moving notation types into grammar rule.ppedrot
2013-11-09Cleaning and documenting Egramcoq.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
2013-07-17More dynamic argument scopesletouzey
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-03-17Avoid a few overzealous "when Errors.noncritical"letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-05More monomorphization.ppedrot
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:09:18 +0000