aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2018-01-20Fix #6618: coqchk fails with "ill-typed term".Pierre-Marie Pédrot
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
2018-01-10Add interfaces for checker and remove dead code.Maxime Dénès
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-05Merge PR #6266: Safe unmarshalling in the checkerMaxime Dénès
2017-12-02Remove redundant Zcase from the checker.Pierre-Marie Pédrot
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-11-29Forbid implicitly relative names in the checker.Pierre-Marie Pédrot
2017-11-29Mark the -I option in coqchk as deprecated and merge it with -Q.Pierre-Marie Pédrot
2017-11-29Add a -Q option to coqchck.Pierre-Marie Pédrot
2017-11-29Allow to pass physical files to coqchk.Pierre-Marie Pédrot
2017-11-28Adding an interface file for checker/check.ml.Pierre-Marie Pédrot
2017-11-28Use safe demarshalling in the checker.Pierre-Marie Pédrot
2017-11-28Use large arrays in the checker demarshaller.Pierre-Marie Pédrot
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 04:18:20 +0000