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
*
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
|
|
*
|
[notation] Allow to retrieve defined notations.
Emilio Jesus Gallego Arias
2016-09-25
|
|
/
/
*
|
|
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
\
\
*
|
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
*
|
|
|
Changing the definition of the "Lib.variable.info" type to enable us to do mo...
Matej Kosik
2016-08-24
|
|
/
/
|
/
|
|
|
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
*
|
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
*
|
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
/
[next]