index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
metasyntax.ml
Age
Commit message (
Expand
)
Author
2017-09-12
Fixing bug #5693 (treating empty notation format as any format).
Hugo Herbelin
2017-08-29
Quoting notations in incompatible-level error message.
Hugo Herbelin
2017-08-29
A new step of restructuration of notations.
Hugo Herbelin
2017-08-29
Dropping former fix to bug #5469 (notation format not recognizing curly braces).
Hugo Herbelin
2017-08-29
A little reorganization of notations + a fix to #5608.
Hugo Herbelin
2017-08-01
Merge PR #834: Adding support for recursive notations of the form "x , .. , y...
Maxime Dénès
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-26
Adding support for recursive notations of the form "x , .. , y , z".
Hugo Herbelin
2017-07-04
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-08
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-04-27
Remove some unused values and types
Gaetan Gilbert
2017-04-27
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-25
[location] [ast] Switch Constrexpr AST to an extensible node type.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-24
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-15
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-22
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-02-15
[stm] Break stm/toplevel dependency loop.
Emilio Jesus Gallego Arias