aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2017-11-23Truncate strings in votour to 1024 characters.Pierre-Marie Pédrot
2017-11-23Bypass int and string representation in votour when it's incorrect.Pierre-Marie Pédrot
2017-11-23Tail-recursive list traversal in votour.Pierre-Marie Pédrot
2017-11-22Implement a tail-recursive traversal of the object in votour.Pierre-Marie Pédrot
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
2017-09-21Fix -silent flag of coqchk after ff918e4.Maxime Dénès
2017-09-21Adapt checker to change in locations.Maxime Dénès
2017-09-21[checker] Add missing Feedback printer (BZ#5587)Emilio Jesus Gallego Arias
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-09-15Merge PR #955: Do not hashcons universes beforehandMaxime Dénès
2017-09-01Do not hashcons universes beforehand.Pierre-Marie Pédrot
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the checker.Pierre-Marie Pédrot
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16A short cleanupAmin Timany
2017-06-16use map_constr more efficientlyAmin Timany
2017-06-16OptimizationAmin Timany
2017-06-16Use a smart map_constrAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Checker add test for non-trivial constraintsAmin Timany
2017-06-16Properly instantiate contexts before pushingAmin Timany
2017-06-16Enable the checking of ind subtyping in checkerAmin Timany
2017-06-16Correct coqchk checking subtyping relation for inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-29Merge PR#512: [cleanup] Unify all calls to the error function.Maxime Dénès
2017-05-28Fix a bug in checkerAmin Timany
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-26[checker] [votour] resolve warning 52 fragile constant patternGaëtan Gilbert
2017-05-26[votour] Fix/disable warnings.Emilio Jesus Gallego Arias
2017-05-26[votour] Fix build with -safe-string (bug 5553)Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-03Merge PR#411: Mention template polymorphism in the documentation.Maxime Dénès
2017-05-02Merge PR#582: Fix warningsMaxime Dénès
2017-05-01More consistent writing of de Bruijn.Théo Zimmermann
2017-04-27Remove uses of [Flags.make_silent]Gaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 09:15:22 +0000