aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Merge PR #1075: Re-enable checker error messagesGravatar Maxime Dénès2017-09-25
|\
| * Fix -silent flag of coqchk after ff918e4.Gravatar Maxime Dénès2017-09-21
| * Adapt checker to change in locations.Gravatar Maxime Dénès2017-09-21
| * [checker] Add missing Feedback printer (BZ#5587)Gravatar Emilio Jesus Gallego Arias2017-09-21
* | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/
* Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\
| * Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
* | Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* | Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
|/
* Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\
| * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
* | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/
* Fixing the checker w.r.t. wrongly used abstract universe contexts.Gravatar Pierre-Marie Pédrot2017-07-19
* Properly handling polymorphic inductive subtyping in the checker.Gravatar Pierre-Marie Pédrot2017-07-11
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A short cleanupGravatar Amin Timany2017-06-16
* use map_constr more efficientlyGravatar Amin Timany2017-06-16
* OptimizationGravatar Amin Timany2017-06-16
* Use a smart map_constrGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
* Properly instantiate contexts before pushingGravatar Amin Timany2017-06-16
* Enable the checking of ind subtyping in checkerGravatar Amin Timany2017-06-16
* Correct coqchk checking subtyping relation for inductivesGravatar Amin Timany2017-06-16
* Correct coqchk reductionGravatar Amin Timany2017-06-16
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\ \
| | * Fix a bug in checkerGravatar Amin Timany2017-05-28
| * | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | [checker] [votour] resolve warning 52 fragile constant patternGravatar Gaëtan Gilbert2017-05-26
* | | [votour] Fix/disable warnings.Gravatar Emilio Jesus Gallego Arias2017-05-26
* | | [votour] Fix build with -safe-string (bug 5553)Gravatar Emilio Jesus Gallego Arias2017-05-26
|/ /
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| * \ Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\ \
| * \ \ Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\ \ \
| * | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | * | | Remove uses of [Flags.make_silent]Gravatar Gaetan Gilbert2017-04-27
| | * | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | * | | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| | * | | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
| |/ / /
* / / / [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ / /
| * / Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ /
* | [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Merge remote-tracking branch 'github/pr/257' into v8.6Gravatar Maxime Dénès2016-09-30
| |\