index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_constr.ml4
Commit message (
Expand
)
Author
Age
*
Remove reference name type.
Maxime Dénès
2018-06-18
*
[api] Misctypes removal: several moves:
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Remove deprecated object from `Term`
Emilio Jesus Gallego Arias
2018-05-30
*
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
Trying a hack to support {'pat|P} without breaking compatibility.
Hugo Herbelin
2018-02-20
*
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
*
Adding patterns in the category of binders for notations.
Hugo Herbelin
2018-02-20
*
Removing cumbersome location in multiple patterns.
Hugo Herbelin
2017-12-12
*
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
*
A cosmetic standardization: adding a space in g_constr.ml4.
Hugo Herbelin
2017-11-27
*
Releasing level "11" of "pattern".
Hugo Herbelin
2017-11-27
*
Fixing associativity registered for level 10.
Hugo Herbelin
2017-11-27
*
Merge PR #1094: Fixing a little parsing bug with level 90 introduced in 3e70e...
Maxime Dénès
2017-10-03
|
\
|
*
Fixing a little parsing bug with level 90 introduced in 3e70ea9c.
Hugo Herbelin
2017-09-25
*
|
Allow empty instance parsing @{}
Matthieu Sozeau
2017-09-19
|
/
*
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-09-08
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)
Pierre Letouzey
2017-06-14
*
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
|
*
Allow flexible anonymous universes in instances and sorts.
Gaetan Gilbert
2017-05-03
*
|
[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-25
*
|
[location] More located use.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[location] Use Loc.located for constr_expr.
Emilio Jesus Gallego Arias
2017-04-24
*
|
[constrexpr] Make patterns use Loc.located for location information
Emilio Jesus Gallego Arias
2017-04-24
|
/
*
Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...
Maxime Dénès
2017-04-12
|
\
*
|
[camlpX] Remove camlp4 compat layer.
Emilio Jesus Gallego Arias
2017-04-07
*
|
Applying same convention as in Definition for parsing type in a let in.
Hugo Herbelin
2017-03-24
*
|
Replacing "cast surgery" in LetIn by a proper field (see PR #404).
Hugo Herbelin
2017-03-24
*
|
Unifying standard "constr_level" names for constructors of local_binder_expr.
Hugo Herbelin
2017-03-24
*
|
"Standardizing" the name LocalPatten into LocalRawPattern.
Hugo Herbelin
2017-03-24
|
*
Supporting arbitrary binders in record fields, including e.g. patterns.
Hugo Herbelin
2017-03-23
|
*
Removing a redundant line in the syntax of record fields.
Hugo Herbelin
2017-03-23
|
*
Improving the API of constrexpr_ops.mli.
Hugo Herbelin
2017-03-23
|
/
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
*
Fix bug #4869, allow Prop, Set, and level names in constraints.
Matthieu Sozeau
2016-09-29
*
|
Moving the tactic-in-term extension from G_constr to G_ltac.
Pierre-Marie Pédrot
2016-09-14
*
|
Make the user_err header an optional parameter.
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
*
Adding ability to put any pattern in binders, prefixed by a quote.
Daniel de Rauglaudre
2016-06-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
*
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
Adopting the same rules for interpreting @, abbreviations and
Hugo Herbelin
2016-03-13
*
|
Supporting "(@foo) args" in patterns, where "@foo" has no arguments.
Hugo Herbelin
2016-03-13
*
|
Uniformizing the parsing of argument scopes in Ltac.
Pierre-Marie Pédrot
2016-03-04
[next]