index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Removing the uses of abstraction-breaking code in Obligations.
Pierre-Marie Pédrot
2017-07-13
*
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
*
The only abstraction-breaking function in Univ is now AUContext.instance.
Pierre-Marie Pédrot
2017-07-13
*
Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Elimschemes.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Discharge.
Pierre-Marie Pédrot
2017-07-13
*
Make the typeclass implementation fully compatible with universe polymorphism.
Pierre-Marie Pédrot
2017-07-13
*
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-13
*
Safer API for Global.type_of_global_in_context.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Record.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Search.
Pierre-Marie Pédrot
2017-07-13
*
Getting rid of AUContext abstraction breakers in Recordops.
Pierre-Marie Pédrot
2017-07-13
*
Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel
Maxime Dénès
2017-07-13
|
\
|
*
Adding a comment regarding De Bruijn universe indices in the kernel.
Pierre-Marie Pédrot
2017-07-12
*
|
Merge PR #871: Update Travis badge following the switch to master
Maxime Dénès
2017-07-11
|
\
\
|
*
|
Update Travis badge following the switch to master
Théo Zimmermann
2017-07-11
|
|
*
Moving the last bits of abtraction-breaking code out of the kernel.
Pierre-Marie Pédrot
2017-07-11
|
|
*
Fix nonsensical universe abstraction in the kernel.
Pierre-Marie Pédrot
2017-07-11
|
|
*
Properly handling polymorphic inductive subtyping in the checker.
Pierre-Marie Pédrot
2017-07-11
|
|
*
Properly handling polymorphic inductive subtyping in the kernel.
Pierre-Marie Pédrot
2017-07-11
|
|
*
Cleaning up the implementation of module subtyping in the kernel.
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
|
|
*
Asserting that monomorphic section variables have no abstracted context.
Pierre-Marie Pédrot
2017-07-11
|
|
*
Getting rid of simple calls to AUContext.instance.
Pierre-Marie Pédrot
2017-07-11
|
|
/
*
|
Merge branch 'v8.7'
Maxime Dénès
2017-07-11
|
\
\
|
|
/
|
/
|
|
*
Merge PR #858: [travis] Remove CompCert version check hack.
Maxime Dénès
2017-07-11
|
|
\
*
|
\
Merge PR #867: Removing a redundant universe instance information in native c...
Maxime Dénès
2017-07-11
|
\
\
\
|
|
*
\
Merge PR #860: use Int.equal instead of polymorphic =
Maxime Dénès
2017-07-11
|
|
|
\
\
|
*
|
|
|
Removing a redundant universe instance information in native compute.
Pierre-Marie Pédrot
2017-07-10
|
/
/
/
/
|
*
|
|
Merge PR #863: Fixing environment in warning "Projection value has no head co...
Maxime Dénès
2017-07-07
|
|
\
\
\
|
*
\
\
\
Merge PR #842: Update the Tutorial.
Maxime Dénès
2017-07-07
|
|
\
\
\
\
|
*
\
\
\
\
Merge PR #816: In enter_one, not having exactly one goal is a fatal error of ...
Maxime Dénès
2017-07-07
|
|
\
\
\
\
\
|
*
\
\
\
\
\
Merge PR #835: Remove doc/refman/RefMan-ind.tex
Maxime Dénès
2017-07-07
|
|
\
\
\
\
\
\
|
*
|
|
|
|
|
|
Set version to 8.7.0~alpha.
Maxime Dénès
2017-07-07
|
*
|
|
|
|
|
|
Merge PR #844: Better support for make TIMED=1 on Windows
Maxime Dénès
2017-07-07
|
|
\
\
\
\
\
\
\
|
*
\
\
\
\
\
\
\
Merge PR #800: Enable fiat-crypto
Maxime Dénès
2017-07-07
|
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
|
Fixing environment in warning "Projection value has no head constant".
Hugo Herbelin
2017-07-07
*
|
|
|
|
|
|
|
|
|
Merge PR #853: Clean 'with Definition' implementation.
Maxime Dénès
2017-07-06
|
\
\
\
\
\
\
\
\
\
\
|
|
/
/
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
use Int.equal instead of polymorphic =
Paul Steckler
2017-07-05
|
|
|
|
|
|
|
|
|
*
[travis] Remove CompCert version check hack.
Emilio Jesus Gallego Arias
2017-07-05
|
|
|
|
|
|
|
|
|
/
*
|
|
|
|
|
|
|
|
Merge PR #837: Add inversion_sigma to CHANGES and to doc
Maxime Dénès
2017-07-05
|
\
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn
Maxime Dénès
2017-07-05
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #840: Quote $(OCAMLFIND) in CoqMakefile.in for Windows
Maxime Dénès
2017-07-05
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #839: Update .gitignore with doc/tutorial/Tutorial.v.out
Maxime Dénès
2017-07-05
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #832: Document an example `Makefile` for `coq_makefile`
Maxime Dénès
2017-07-05
|
\
\
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
|
|
|
|
Revert fiat-crypto overlay
Jason Gross
2017-07-04
|
|
_
|
_
|
_
|
_
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
|
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
\
\
\
\
\
\
\
\
\
\
\
*
|
|
|
|
|
|
|
|
|
|
|
|
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Removing dead code in Subtyping.
Pierre-Marie Pédrot
2017-07-04
[next]
Pierre-Marie Pédrot
Maxime Dénès
Théo Zimmermann
Hugo Herbelin
Paul Steckler
Emilio Jesus Gallego Arias
Jason Gross