index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-03-15
Adding a function to encode/decode string list into a single string.
Hugo Herbelin
2020-03-14
Fixes #11692 (clear dependent knows about let-in).
Hugo Herbelin
2020-03-14
Merge PR #10858: Implementing postponed constraints in TC resolution
Gaëtan Gilbert
2020-03-13
Merge PR #11797: Dune build rules for doc_grammar and fullGrammar.
Emilio Jesus Gallego Arias
2020-03-13
Merge PR #11688: When parsing a negative integer, ensure that the minus sign ...
Emilio Jesus Gallego Arias
2020-03-13
Merge PR #11803: Update Azure MacOS version 10.13 -> 10.14
Emilio Jesus Gallego Arias
2020-03-13
[funind] [cleanup] Remove unused function parameters
Emilio Jesus Gallego Arias
2020-03-13
Implementing postponed constraints in TC resolution
Matthieu Sozeau
2020-03-13
Update Azure MacOS version 10.13 -> 10.14
Gaëtan Gilbert
2020-03-13
Merge PR #11805: Fix coqchk for primitive integers on 32bit arch with OCaml >...
Pierre-Marie Pédrot
2020-03-13
Merge PR #11016: [proof] Remove duplication in the proof save path.
Gaëtan Gilbert
2020-03-13
Merge PR #11804: [CI] test hierarchy builder as part of elpi
Gaëtan Gilbert
2020-03-13
Merge PR #11815: [ci] [doc] Point to actual docker instructions.
Gaëtan Gilbert
2020-03-13
Merge PR #11003: [vernac] Remove deprecated function.
Gaëtan Gilbert
2020-03-13
[cleanup] Remove unnecessary Map/Set module creation
Emilio Jesus Gallego Arias
2020-03-13
Fixing a non-protected try-with in class_tactics.ml.
Hugo Herbelin
2020-03-13
Double-checking at tclZERO entry that the exception is non critical.
Hugo Herbelin
2020-03-13
Deprecation of catchable_exception, to be replaced by noncritical in try-with.
Hugo Herbelin
2020-03-13
Removing catchable_exception test in tclOR/tclORELSE.
Hugo Herbelin
2020-03-13
Replacing catchable_exception by noncritical in try-with blocks.
Hugo Herbelin
2020-03-13
[lemmas] Consolidate some declaration data on Info.t
Emilio Jesus Gallego Arias
2020-03-12
[declare] Remove trivial wrapper
Emilio Jesus Gallego Arias
2020-03-12
[lemmas] Handle mutual lemmas more uniformly.
Emilio Jesus Gallego Arias
2020-03-12
[save proof] Declare universe_binders unconditionally for mutual assumptions.
Emilio Jesus Gallego Arias
2020-03-12
[proof] Remove duplication in the proof save path.
Emilio Jesus Gallego Arias
2020-03-12
[vernac] Minor cleanup of opens in `Vernacentries`
Emilio Jesus Gallego Arias
2020-03-12
Merge PR #11796: Remove parallel building of Sphinx documentation.
Emilio Jesus Gallego Arias
2020-03-12
[ci] [doc] Point to actual docker instructions.
Emilio Jesus Gallego Arias
2020-03-12
Update doc/sphinx/addendum/extended-pattern-matching.rst
larsr
2020-03-12
Fixed link to "match" syntax.
larsr
2020-03-12
Merge PR #11798: Tests make bytecode
Enrico Tassi
2020-03-12
Merge PR #11781: Minor improvements to the unreleased changelog.
Clément Pit-Claudel
2020-03-12
Merge PR #11780: Minor improvements to the unreleased changelog.
Clément Pit-Claudel
2020-03-12
Merge PR #11810: [dune] Fix ocamlopt_flags for release profile
Théo Zimmermann
2020-03-12
Documenting when exceptions are noncritical in the proof engine
Hugo Herbelin
2020-03-12
Add changelog
SimonBoulier
2020-03-12
Add message at the end of search results about implicit arguments
SimonBoulier
2020-03-12
Print implicit arguments in types of references
SimonBoulier
2020-03-12
Dune build rules for doc_grammar and fullGrammar.
Théo Zimmermann
2020-03-12
Add changelog entry
SimonBoulier
2020-03-12
Remove a positivity check when Check Positivity is off
SimonBoulier
2020-03-12
[dune] Fix ocamlopt_flags for release profile
Emilio Jesus Gallego Arias
2020-03-11
Merge PR #11754: [micromega] Add numerical compatibility layer.
Frédéric Besson
2020-03-11
Merge PR #11800: [ci] [gitlab] Move VST to `allow_failure`
Gaëtan Gilbert
2020-03-11
Update dev/ci/ci-basic-overlay.sh
Enrico Tassi
2020-03-11
Fix coqchk for primitive integers on 32bit arch with OCaml >= 4.08 (#11624)
Pierre Roux
2020-03-11
[CI] test hierarchy builder as part of elpi
Enrico Tassi
2020-03-11
Comment difference between the 2 hashes on constr
Gaëtan Gilbert
2020-03-11
Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constants
Pierre-Marie Pédrot
2020-03-11
Merge PR #11786: Fix #11730: Mangle Names vs Infix
Pierre-Marie Pédrot
[prev]
[next]