aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.mli
Commit message (Expand)AuthorAge
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Gravatar Maxime Dénès2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
* A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
* Selecting which notation to print based on current stack of scope.Gravatar Hugo Herbelin2017-11-27
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* A new step of restructuration of notations.Gravatar Hugo Herbelin2017-08-29
* A little reorganization of notations + a fix to #5608.Gravatar Hugo Herbelin2017-08-29
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| |\
* | | Notation.declare_rawnumeral_interpreterGravatar Pierre Letouzey2017-06-14
| * | Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Paul Steckler2017-06-09
| | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |/
* | 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