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
*
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
|
/
/
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Fixing #4865 (deciding on which arguments to recompute scopes was not robust).
Hugo Herbelin
2016-06-29
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Properly handling the only printing flag when parsing rules already exist.
Pierre-Marie Pédrot
2016-06-28
*
|
Removing the use to Egramcoq.recover_constr_grammar.
Pierre-Marie Pédrot
2016-06-07
|
*
Remove tabulation support from pretty-printing.
Guillaume Melquiond
2016-06-02
|
/
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Revert "A heuristic to add parentheses in the presence of rules such as"
Hugo Herbelin
2016-04-27
[next]