index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
notation.ml
Commit message (
Expand
)
Author
Age
*
[notations] Split interpretation and parsing of notations
Emilio Jesus Gallego Arias
2018-05-31
*
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
*
Removing a superfluous trailing newline in "Locate" for a notation.
Hugo Herbelin
2018-05-13
*
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Hugo Herbelin
2018-05-10
*
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
Hugo Herbelin
2018-05-10
*
[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.
Emilio Jesus Gallego Arias
2018-05-04
*
Revert "Merge PR #873: New strategy based on open scopes for deciding which n...
Maxime Dénès
2018-03-09
*
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-05
|
\
*
|
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-28
|
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Hugo Herbelin
2018-02-20
*
Notations: A step in cleaning constr_entry_key.
Hugo Herbelin
2018-02-20
*
More flexibility in locating or referring to a notation.
Hugo Herbelin
2018-02-20
*
Respecting the ident/pattern distinction in notation modifiers.
Hugo Herbelin
2018-02-20
*
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
*
Allows recursive patterns for binders to be associative on the left.
Hugo Herbelin
2018-02-20
*
Selecting which notation to print based on current stack of scope.
Hugo Herbelin
2017-11-27
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Adding a missing period in a notation warning.
Hugo Herbelin
2017-09-12
*
Making detyping potentially lazy.
Pierre-Marie Pédrot
2017-09-04
*
A new step of restructuration of notations.
Hugo Herbelin
2017-08-29
*
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-08-29
*
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
*
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
*
Merge PR#713: Bump year in headers.
Maxime Dénès
2017-06-15
|
|
\
*
|
|
Notation.declare_rawnumeral_interpreter
Pierre Letouzey
2017-06-14
*
|
|
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
Pierre Letouzey
2017-06-14
|
*
|
Fix Bug #5568, no dup notation warnings on repeated module imports
Paul Steckler
2017-06-09
*
|
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
|
*
Bump year in headers.
Maxime Dénès
2017-06-01
|
|
/
*
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
|
*
|
[interp] [ast] Make raw_cases_pattern_expr private.
Emilio Jesus Gallego Arias
2017-05-15
|
*
|
Fix 4.04 warnings
Gaetan Gilbert
2017-04-27
*
|
|
[location] [ast] Port module AST to CAst
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
*
|
|
[location] Switch glob_constr to Loc.located
Emilio Jesus Gallego Arias
2017-04-24
*
|
|
[location] Move Glob_term.cases_pattern to located.
Emilio Jesus Gallego Arias
2017-04-24
*
|
|
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-24
|
/
/
*
|
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-24
|
\
\
|
*
\
Merge PR#189: Remove tabulation support from pretty-printing.
Maxime Dénès
2017-02-20
|
|
\
\
*
|
|
|
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
*
|
|
|
Classops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
|
|
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
/
/
/
*
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-17
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Merge PR #289 into v8.6.
Pierre-Marie Pédrot
2016-10-12
|
|
\
\
*
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
|
|
|
*
|
|
Warning about similar notations now up to alpha-conversion.
Hugo Herbelin
2016-09-28
[next]