aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
Commit message (Expand)AuthorAge
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Adding a test to check whether two tactic notations conflict.Gravatar Pierre-Marie Pédrot2015-05-11
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-11
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-04
* Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Gravatar Enrico Tassi2015-02-03
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-03
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* Now printing "now a keyword" only in verbose mode.Gravatar Hugo Herbelin2014-10-17
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Additional entry tactic_arg in Print Grammar tactic.Gravatar Pierre-Marie Pédrot2014-09-03
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Qualified ML tactic names. The plugin name is used to discriminateGravatar Pierre-Marie Pédrot2014-07-27
* Useless keeping of dirpath in tactic aliases.Gravatar Pierre-Marie Pédrot2014-06-30
* Fix the behaviour of ML tactic notations w.r.t. Imports by making themGravatar Pierre-Marie Pédrot2014-05-13
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
* Fixing printing of only_parsing notations.Gravatar Pierre-Marie Pédrot2014-02-25
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* Moving notation types into grammar rule.Gravatar ppedrot2013-11-09
* Cleaning and documenting Egramcoq.Gravatar ppedrot2013-11-09
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* More dynamic argument scopesGravatar letouzey2013-07-17
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Avoid a few overzealous "when Errors.noncritical"Gravatar letouzey2013-03-17
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* More monomorphization.Gravatar ppedrot2013-03-05
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Fixed bug #2967 (some missing check on ill-formed recursive notation strings).Gravatar herbelin2013-01-27
* Modulification of identifierGravatar ppedrot2012-12-14
* Using library string functions.Gravatar ppedrot2012-12-13
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Revised the strategy for automatic insertion of spaces when printingGravatar herbelin2012-12-04
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-13 19:23:04 +0000