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
...
*
|
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
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-06-08
|
\
*
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
|
Merge PR#512: [cleanup] Unify all calls to the error function.
Maxime Dénès
2017-05-29
|
\
\
|
|
*
Fix a bug in checker
Amin Timany
2017-05-28
|
*
|
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
|
|
[checker] [votour] resolve warning 52 fragile constant pattern
Gaë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-26
|
/
/
*
|
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
|
\
\
[prev]
[next]