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
*
Moving Rtree.smart_map into Rtree.Smart.map.
Hugo Herbelin
2018-05-23
*
Moving Option.smart_map to Option.Smart.map.
Hugo Herbelin
2018-05-23
*
Collecting List.smart_* functions into a module List.Smart.
Hugo Herbelin
2018-05-23
*
Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.
Hugo Herbelin
2018-05-23
*
Collecting Array.smart_* functions into a module Array.Smart.
Hugo Herbelin
2018-05-23
*
Emphasizing the "smart"ness of Array.smartfoldmap{,2} in their documentation.
Hugo Herbelin
2018-05-23
*
CArray: adding combinators.
Hugo Herbelin
2018-05-23
*
Merge PR #7414: Add .byte targets for every bestocaml target
Enrico Tassi
2018-05-23
|
\
*
\
Merge PR #7567: Clean-up dead file in test-suite.
Enrico Tassi
2018-05-23
|
\
\
*
\
\
Merge PR #7565: Document the new nested-proof error message.
Emilio Jesus Gallego Arias
2018-05-22
|
\
\
\
*
\
\
\
Merge PR #7577: Fixing debugger after #6859 (loading dynlink.cma before lib.c...
Emilio Jesus Gallego Arias
2018-05-22
|
\
\
\
\
|
*
|
|
|
Fixing debugger after #6859 (loading dynlink.cma before lib.cma).
Hugo Herbelin
2018-05-22
*
|
|
|
|
Merge PR #7384: Split Universes
Pierre-Marie Pédrot
2018-05-22
|
\
\
\
\
\
|
|
/
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #7324: Infrastructure for ocamldebug on the checker
Hugo Herbelin
2018-05-22
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7526: [circle] Use Docker image from Gitlab registry.
Gaëtan Gilbert
2018-05-22
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7568: [ci] [gitlab] Fix printenv sorting for variables that span mu...
Gaëtan Gilbert
2018-05-22
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6859: [stm] Make toplevels standalone executables.
Théo Zimmermann
2018-05-22
|
\
\
\
\
\
\
\
\
|
|
*
|
|
|
|
|
|
[ci] [gitlab] Fix printenv sorting for variables that span multiple lines.
Emilio Jesus Gallego Arias
2018-05-21
|
|
/
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
|
|
Document the new nested-proof error message.
Théo Zimmermann
2018-05-21
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
[ide] Remove special option `-ideslave`
Emilio Jesus Gallego Arias
2018-05-21
|
*
|
|
|
|
|
[stm] Make toplevels standalone executables.
Emilio Jesus Gallego Arias
2018-05-21
|
*
|
|
|
|
|
[ci] Add Dune to the base system.
Emilio Jesus Gallego Arias
2018-05-21
|
/
/
/
/
/
/
*
|
|
|
|
|
Merge PR #7557: Add test cases from #7554
Théo Zimmermann
2018-05-20
|
\
\
\
\
\
\
|
*
|
|
|
|
|
Add test cases from #7554
Tej Chajed
2018-05-20
*
|
|
|
|
|
|
Merge PR #7527: [windows] Don't build menhir and int anymore in the packaging...
Michael Soegtrop
2018-05-19
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #7550: [CI] Fix the script used by math-classes.
Emilio Jesus Gallego Arias
2018-05-18
|
\
\
\
\
\
\
\
\
|
|
_
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
Merge PR #6965: [api] Move universe syntax to `Glob_term`
Pierre-Marie Pédrot
2018-05-18
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
|
Clean-up dead file in test-suite.
Théo Zimmermann
2018-05-18
|
|
_
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
[CI] Fix the script used by math-classes.
Pierre-Marie Pédrot
2018-05-18
|
|
/
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
*
|
Split off Universes functions for minimization.
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Make Universes.refresh_constraints internal to UState
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Split off Universes functions about substitutions and constraints
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Remove unused argument to solve_constraints_system
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Move solve_constraint_system near its only use site (comInductive)
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Split off Universes functions dealing with generating new universes.
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Split off Universes functions dealing with names.
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Stop using Universes.subst(_opt)_univs_constr
Gaëtan Gilbert
2018-05-17
|
|
|
|
|
*
|
Make set minimization option internal to Universes
Gaëtan Gilbert
2018-05-17
|
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
[circle] Use Docker image from Gitlab registry.
Emilio Jesus Gallego Arias
2018-05-17
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #7451: Introduce an option to allow nested lemma, and turn it off by...
Emilio Jesus Gallego Arias
2018-05-17
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7359: Reduce usage of evar_map references
Pierre-Marie Pédrot
2018-05-17
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefiniti...
Pierre-Marie Pédrot
2018-05-17
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6870: [ide] Don't set `quiet` on start.
Enrico Tassi
2018-05-17
|
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
Merge PR #7525: [ci] Try to build more of fiat-crypto.
Gaëtan Gilbert
2018-05-17
|
\
\
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
\
\
Merge PR #6808: Add unit tests to test-suite
Gaëtan Gilbert
2018-05-17
|
\
\
\
\
\
\
\
\
\
\
|
|
|
|
|
|
*
|
|
|
|
Document nested proofs and associated option.
Théo Zimmermann
2018-05-17
|
|
|
|
|
|
*
|
|
|
|
[STM] Nested Proofs Allowed has to be executed immediately
Enrico Tassi
2018-05-17
|
|
|
|
|
|
*
|
|
|
|
Remove deprecation warning for nested proofs.
Théo Zimmermann
2018-05-17
|
|
|
|
|
|
*
|
|
|
|
Introduce an option to allow nested lemma, and turn it off by default.
Théo Zimmermann
2018-05-17
|
|
_
|
_
|
_
|
_
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
|
|
|
|
|
|
Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.
Maxime Dénès
2018-05-16
|
\
\
\
\
\
\
\
\
\
\
[next]
Hugo Herbelin
Enrico Tassi
Emilio Jesus Gallego Arias
Pierre-Marie Pédrot
Gaëtan Gilbert
Théo Zimmermann
Tej Chajed
Michael Soegtrop
Maxime Dénès