aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* | [location] Fix warnings.Gravatar Emilio Jesus Gallego Arias2017-05-24
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/
| * Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...Gravatar Maxime Dénès2017-04-28
| |\
* | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ /
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \
| | * More explicit message when a {struct x} argument refers to a local definition.Gravatar Hugo Herbelin2017-04-09
| |/ |/|
| * Fixing #5454 (an assert false with 'pat).Gravatar Hugo Herbelin2017-04-05
* | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
* | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
* | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
|\|
| * Turning an anomaly on 'pat into a proper "unsupported" error message.Gravatar Hugo Herbelin2017-02-09
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\|
| * Fixing #5326 (anomaly on some unsupported case of 'pat).Gravatar Hugo Herbelin2017-01-26
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Shorter message for "Test Asymmetric Patterns".Gravatar Hugo Herbelin2016-10-12
* | Fix an error-prone error API.Gravatar Pierre-Marie Pédrot2016-09-21
* | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
* Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* A more explicit name to the asymmetric boolean flag.Gravatar Hugo Herbelin2016-03-12
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fixing #4467 (continued).Gravatar Hugo Herbelin2016-01-13
| * Fixing #4467 (missing shadowing of variables in cases pattern).Gravatar Hugo Herbelin2016-01-12
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Fixing #3292 (locations of notations shifted by 1 in glob files in trunk).Gravatar Hugo Herbelin2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 13:39:57 +0000