aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
Commit message (Expand)AuthorAge
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Removing a superfluous trailing newline in "Locate" for a notation.Gravatar Hugo Herbelin2018-05-13
* Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Gravatar Hugo Herbelin2018-05-10
* Fixes part 1 of #7462 (only-printing not to override existing interp rule).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
|/
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
* More flexibility in locating or referring to a notation.Gravatar Hugo Herbelin2018-02-20
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Allows recursive patterns for binders to be associative on the left.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
* Adding a missing period in a notation warning.Gravatar Hugo Herbelin2017-09-12
* 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
* Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* 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
* | | Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| * | Fix Bug #5568, no dup notation warnings on repeated module importsGravatar Paul Steckler2017-06-09
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | * 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
| * | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ /
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| * \ Merge PR#189: Remove tabulation support from pretty-printing.Gravatar Maxime Dénès2017-02-20
| |\ \
* | | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Classops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|/ / /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\ \ \ | | |/ | |/|
| * | Merge PR #289 into v8.6.Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| | |
| * | | Warning about similar notations now up to alpha-conversion.Gravatar Hugo Herbelin2016-09-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 12:28:52 +0000