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
*
[refman] Expand a little on global universes.
Matthieu Sozeau
2017-12-01
*
Tests for global universe declarations
Matthieu Sozeau
2017-12-01
*
Proper nametab handling of global universe names
Matthieu Sozeau
2017-12-01
*
Merge PR #736: [ci] Test coqchk on the CompCert target.
Maxime Dénès
2017-12-01
|
\
*
\
Merge PR #6256: CI: better ocaml warning checks
Maxime Dénès
2017-12-01
|
\
\
*
\
\
Merge PR #6276: Coqchk accepts filenames
Maxime Dénès
2017-12-01
|
\
\
\
*
\
\
\
Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...
Maxime Dénès
2017-12-01
|
\
\
\
\
*
\
\
\
\
Merge PR #1049: Remove obsolete locality
Maxime Dénès
2017-11-30
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6244: [lib] [api] Introduce record for `object_prefix`
Maxime Dénès
2017-11-30
|
\
\
\
\
\
\
|
|
|
|
|
|
*
[ci] Test coqchk on the CompCert target.
Théo Zimmermann
2017-11-30
*
|
|
|
|
|
|
Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...
Maxime Dénès
2017-11-30
|
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.
Maxime Dénès
2017-11-30
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...
Maxime Dénès
2017-11-30
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-29
|
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
|
|
[lib] [api] Introduce record for `object_prefix`
Emilio Jesus Gallego Arias
2017-11-29
|
|
|
|
|
*
|
|
[proof] [api] Rename proof types in preparation for functionalization.
Emilio Jesus Gallego Arias
2017-11-29
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #6271: Add PR backport script.
Maxime Dénès
2017-11-29
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...
Maxime Dénès
2017-11-29
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6199: [vernac] Uniformize type of vernac interpretation.
Maxime Dénès
2017-11-29
|
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
|
coq_makefile: pass filenames to coqchk
Ralf Jung
2017-11-29
|
|
|
|
|
|
|
|
*
|
Documenting the possibility to pass filenames to coqchk.
Pierre-Marie Pédrot
2017-11-29
|
|
|
|
|
|
|
|
*
|
Allow to pass physical files to coqchk.
Pierre-Marie Pédrot
2017-11-29
|
|
|
|
|
|
*
|
|
|
In injection/inversion, consider all template-polymorphic types as injectable.
Hugo Herbelin
2017-11-28
|
|
|
|
|
|
*
|
|
|
Adding a variant get_truncation_family_of of get_sort_family_of.
Hugo Herbelin
2017-11-28
|
|
|
|
|
|
*
|
|
|
Moving non-recursive function sort_family_of out of the retype block of recur...
Hugo Herbelin
2017-11-28
|
|
|
|
|
|
|
/
/
/
|
|
|
|
|
|
|
*
/
Adding an interface file for checker/check.ml.
Pierre-Marie Pédrot
2017-11-28
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
|
|
Add PR backport script.
Théo Zimmermann
2017-11-28
|
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
|
|
[ci] [vst] Shorten compilation time to avoid Travis timeouts.
Emilio Jesus Gallego Arias
2017-11-28
|
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
CI: use -byte-only in [warnings] jobs.
Gaëtan Gilbert
2017-11-28
|
|
|
|
|
*
Fix native compute for byte compiled Coq.
Gaëtan Gilbert
2017-11-28
|
|
|
*
|
|
Fix (partial) #4878: option to stop autodeclaring axiom as instance.
Gaëtan Gilbert
2017-11-28
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
Travis: do not build stdlib in [warnings] jobs.
Gaëtan Gilbert
2017-11-28
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #6259: Add PR merge script.
Maxime Dénès
2017-11-28
|
\
\
\
\
|
*
|
|
|
Add PR merge script.
Maxime Dénès
2017-11-28
*
|
|
|
|
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-28
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.
Maxime Dénès
2017-11-28
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6248: [api] Remove aliases of `Evar.t`
Maxime Dénès
2017-11-28
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; up...
Maxime Dénès
2017-11-28
|
\
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
[vernac] Adjust `interp` to pass polymorphic in the attributes.
Emilio Jesus Gallego Arias
2017-11-27
|
|
|
|
|
|
*
|
[vernac] Add polymorphic to the type of vernac interpration options.
Emilio Jesus Gallego Arias
2017-11-27
|
|
|
|
|
|
*
|
[vernac] Start to uniformize type of vernac interpretation.
Emilio Jesus Gallego Arias
2017-11-27
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire...
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
|
|
Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar.
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #6207: [stm] Allow delayed constant in interactive mode.
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
Merge PR #6241: [lib] Generalize Control.timeout type.
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6228: Make byte on gitlab.
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6226: Enhance votour
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
\
\
\
\
Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs
Maxime Dénès
2017-11-27
|
\
\
\
\
\
\
\
\
\
\
\
\
\
\
[next]