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-07-01
UIP in SProp
Gaëtan Gilbert
2020-07-01
Merge PR #12504: [states] Move States to vernac
Gaëtan Gilbert
2020-07-01
Remove deprecated (in 8.8 #6277) coqchk -I
Gaëtan Gilbert
2020-07-01
Merge PR #12605: [test-suite] async-proofs off in tests with Fail Timeout
Gaëtan Gilbert
2020-07-01
Merge PR #12615: [ci] [performance-tests] Use a lighter target.
Gaëtan Gilbert
2020-07-01
Use weak ref to memoize Evarutil.is_ground_env
Gaëtan Gilbert
2020-07-01
Merge PR #12616: [ci] Disable the OCaml 4.12 target
Gaëtan Gilbert
2020-07-01
Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.
Emilio Jesus Gallego Arias
2020-07-01
[ci] Disable the OCaml 4.12 target
Emilio Jesus Gallego Arias
2020-06-30
Cleanup mentions of -as in coqdep usage message
Gaëtan Gilbert
2020-06-30
[ci] [performance-tests] Use a lighter target.
Emilio Jesus Gallego Arias
2020-06-30
docs(README.md): Update badge and links
Erik Martin-Dorel
2020-06-30
Merge PR #12599: Remove the Refiner module
Emilio Jesus Gallego Arias
2020-06-30
[declaremods] Remove abstraction of imperative module operations
Emilio Jesus Gallego Arias
2020-06-30
[states] Move States to vernac
Emilio Jesus Gallego Arias
2020-06-30
Merge PR #11977: Generate default names for bound universes of polymorphic de...
Emilio Jesus Gallego Arias
2020-06-29
[test-suite] async-proofs off in tests with Fail Timeout
Enrico Tassi
2020-06-29
Merge PR #12570: CoqIDE: fix lexing of UTF-8 in quotations like constr:()
Pierre-Marie Pédrot
2020-06-29
Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_list
Pierre-Marie Pédrot
2020-06-29
Adding overlay.
Pierre-Marie Pédrot
2020-06-29
Refining out the Refiner.
Pierre-Marie Pédrot
2020-06-29
Move the FailError exception from Refiner to Tacticals.
Pierre-Marie Pédrot
2020-06-29
Moving the remaining Refiner functions to Tacmach.
Pierre-Marie Pédrot
2020-06-29
Remove Refiner.refiner.
Pierre-Marie Pédrot
2020-06-29
Remove the deprecated functions from refiner, moving them to Tacticals.
Pierre-Marie Pédrot
2020-06-29
Merge PR #12604: Update CAMLDONTLINK in CoqMakefile.in
Enrico Tassi
2020-06-29
Merge PR #12372: [declare] Refactor constant information into a record.
Gaëtan Gilbert
2020-06-28
Update CAMLDONTLINK in CoqMakefile.in
Andres Erbsen
2020-06-27
Merge PR #12518: [ci] [ocaml] Track OCaml 4.12
Gaëtan Gilbert
2020-06-27
Merge PR #12583: [test-suite] Fix dependencies of modules/ files
Gaëtan Gilbert
2020-06-26
Merge PR #12598: Mention VSCoq with respect to _CoqProject
Théo Zimmermann
2020-06-26
Mention VSCoq with respect to _CoqProject
Carl Patenaude-Poulin
2020-06-26
[ci] Add overlays for PR #12372
Emilio Jesus Gallego Arias
2020-06-26
[recLemmas] Nit on naming consistency.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Return list of declared global in Proof.save
Emilio Jesus Gallego Arias
2020-06-26
[declare] Some more cleanup on unused functions after the last commits.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Remove Proof_ending from the public API
Emilio Jesus Gallego Arias
2020-06-26
[declare] Merge remaining obligations bits into Declare
Emilio Jesus Gallego Arias
2020-06-26
[obligation] Switch to new declare info API.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Improve logical code order
Emilio Jesus Gallego Arias
2020-06-26
[declare] Improve organization of proof/constant information.
Emilio Jesus Gallego Arias
2020-06-26
[vernac] Nit refatoring on lemma command interpretation
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on regular lemma init.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Use Recthm.t in mutual analysis functions
Emilio Jesus Gallego Arias
2020-06-26
[declare] Refactor analysis and construction of mutual lemmas
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on hook call.
Emilio Jesus Gallego Arias
2020-06-26
[declare] Nit on interface
Emilio Jesus Gallego Arias
2020-06-26
[declare] Documentation on obligations
Emilio Jesus Gallego Arias
2020-06-26
[declare] [compat] Remove exception alias.
Emilio Jesus Gallego Arias
2020-06-26
[declare] [api] Modify logical presentation of declare interfaces
Emilio Jesus Gallego Arias
[prev]
[next]