index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
Commit message (
Expand
)
Author
Age
*
[lib] Rename Profile to CProfile
Emilio Jesus Gallego Arias
2017-12-09
*
Merge PR #6277: Qualified import in coqchk
Maxime Dénès
2017-12-07
|
\
*
\
Merge PR #6303: Remove redundant Zcase from the checker.
Maxime Dénès
2017-12-07
|
\
\
*
\
\
Merge PR #6266: Safe unmarshalling in the checker
Maxime Dénès
2017-12-05
|
\
\
\
|
|
*
|
Remove redundant Zcase from the checker.
Pierre-Marie Pédrot
2017-12-02
|
|
/
/
|
/
|
|
|
|
*
Documenting the -Q flag of coqchk.
Pierre-Marie Pédrot
2017-12-01
|
|
*
Forbid implicitly relative names in the checker.
Pierre-Marie Pédrot
2017-11-29
|
|
*
Mark the -I option in coqchk as deprecated and merge it with -Q.
Pierre-Marie Pédrot
2017-11-29
|
|
*
Add a -Q option to coqchck.
Pierre-Marie Pédrot
2017-11-29
|
|
/
|
/
|
*
|
Allow to pass physical files to coqchk.
Pierre-Marie Pédrot
2017-11-29
*
|
Adding an interface file for checker/check.ml.
Pierre-Marie Pédrot
2017-11-28
|
*
Use safe demarshalling in the checker.
Pierre-Marie Pédrot
2017-11-28
|
*
Use large arrays in the checker demarshaller.
Pierre-Marie Pédrot
2017-11-28
|
/
*
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-28
|
\
|
*
When declaring constants/inductives use ContextSet if monomorphic.
Gaëtan Gilbert
2017-11-24
*
|
Truncate strings in votour to 1024 characters.
Pierre-Marie Pédrot
2017-11-23
*
|
Bypass int and string representation in votour when it's incorrect.
Pierre-Marie Pédrot
2017-11-23
*
|
Tail-recursive list traversal in votour.
Pierre-Marie Pédrot
2017-11-23
*
|
Implement a tail-recursive traversal of the object in votour.
Pierre-Marie Pédrot
2017-11-22
|
/
*
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Maxime Dénès
2017-11-13
|
\
|
*
[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-11-06
|
/
*
Merge PR #1075: Re-enable checker error messages
Maxime Dénès
2017-09-25
|
\
|
*
Fix -silent flag of coqchk after ff918e4.
Maxime Dénès
2017-09-21
|
*
Adapt 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-21
*
|
[flags] Flag `open Flags`
Emilio Jesus Gallego Arias
2017-09-20
|
/
*
Merge PR #955: Do not hashcons universes beforehand
Maxime Dénès
2017-09-15
|
\
|
*
Do not hashcons universes beforehand.
Pierre-Marie Pédrot
2017-09-01
*
|
Statically enforcing that module types have no retroknowledge.
Pierre-Marie Pédrot
2017-08-29
*
|
Separating the module_type and module_body types by using a type parameter.
Pierre-Marie Pédrot
2017-08-29
|
/
*
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-31
|
\
|
*
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
*
|
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
|
/
*
Fixing the checker w.r.t. wrongly used abstract universe contexts.
Pierre-Marie Pédrot
2017-07-19
*
Properly handling polymorphic inductive subtyping in the checker.
Pierre-Marie Pédrot
2017-07-11
*
Safe API for accessing universe constraints of global references.
Pierre-Marie Pédrot
2017-07-11
*
Less footguns in universe handling: remove subst_instance_context.
Pierre-Marie Pédrot
2017-07-11
*
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
A short cleanup
Amin Timany
2017-06-16
*
use map_constr more efficiently
Amin Timany
2017-06-16
*
Optimization
Amin Timany
2017-06-16
*
Use a smart map_constr
Amin Timany
2017-06-16
*
Clean up universes of constants and inductives
Amin Timany
2017-06-16
*
Checker add test for non-trivial constraints
Amin Timany
2017-06-16
*
Properly instantiate contexts before pushing
Amin Timany
2017-06-16
*
Enable the checking of ind subtyping in checker
Amin Timany
2017-06-16
*
Correct coqchk checking subtyping relation for inductives
Amin Timany
2017-06-16
*
Correct coqchk reduction
Amin Timany
2017-06-16
[next]