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
*
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
|
\
\
|
*
\
Merge PR#411: Mention template polymorphism in the documentation.
Maxime Dénès
2017-05-03
|
|
\
\
|
*
\
\
Merge PR#582: Fix warnings
Maxime Dénès
2017-05-02
|
|
\
\
\
|
*
|
|
|
More consistent writing of de Bruijn.
Théo Zimmermann
2017-05-01
|
|
*
|
|
Remove uses of [Flags.make_silent]
Gaetan Gilbert
2017-04-27
|
|
*
|
|
Remove some unused values and types
Gaetan Gilbert
2017-04-27
|
|
*
|
|
Remove unused [rec] keywords
Gaetan Gilbert
2017-04-27
|
|
*
|
|
Locally disable some warnings.
Gaetan Gilbert
2017-04-27
|
|
/
/
/
*
/
/
/
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-25
|
/
/
/
|
*
/
Update various comments to use "template polymorphism"
Gaetan Gilbert
2017-04-11
|
/
/
*
|
[pp] Remove uses of expensive string_of_ppcmds.
Emilio Jesus Gallego Arias
2017-03-21
*
|
Moving unused code out of the kernel into Termops.
Pierre-Marie Pédrot
2016-10-31
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
|
|
*
Merge remote-tracking branch 'github/pr/257' into v8.6
Maxime Dénès
2016-09-30
|
|
\
[next]