aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.mli
Commit message (Expand)AuthorAge
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * [interp] [ast] Make raw_cases_pattern_expr private.Gravatar Emilio Jesus Gallego Arias2017-05-15
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [notation] Allow to retrieve defined notations.Gravatar Emilio Jesus Gallego Arias2016-09-25
* Properly handling the only printing flag when parsing rules already exist.Gravatar Pierre-Marie Pédrot2016-06-28
* Removing the use to Egramcoq.recover_constr_grammar.Gravatar Pierre-Marie Pédrot2016-06-07
* Revert "A heuristic to add parentheses in the presence of rules such as"Gravatar Hugo Herbelin2016-04-27
* A heuristic to add parentheses in the presence of rules such asGravatar Hugo Herbelin2016-04-27
* Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Gravatar Matthieu Sozeau2016-04-04
|\
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Move type_scope into user space, fix some output logsGravatar Jason Gross2015-08-14
| * Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080Gravatar Jason Gross2015-08-14
|/
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
* Update headers.Gravatar Maxime Dénès2015-01-12
* Notation: option to attach extra pretty printing rules to notationsGravatar Enrico Tassi2014-09-29
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Useless check when loading notations through import.Gravatar Pierre-Marie Pédrot2014-03-01
* Reverting the old LIFO behaviour of the notation finding algorithm.Gravatar ppedrot2013-11-08
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* More equality functionsGravatar ppedrot2012-11-25
* Taking into account the type of a definition (if it exists), and theGravatar herbelin2012-11-17
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
* Noise for nothingGravatar pboutill2012-03-02
* New Arguments vernacularGravatar gareuselesinge2011-11-21
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Optimized need for delimiters when disjoint scopes for strings andGravatar herbelin2010-04-10
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Fix a small notation/scope bug:Gravatar vsiles2009-04-30