aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.mli
Commit message (Expand)AuthorAge
* 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
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
* Utilisation du section_path pour le parsing des notations primitives,Gravatar herbelin2006-02-04
* Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...Gravatar herbelin2006-01-08
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02