index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-09-24
Merge PR #10774: Make `zify` does work for `Z.to_N`
Frédéric Besson
2019-09-24
Merge PR #10699: [gitlab/ci] Prevent Corn from running if Bignums has failed.
Gaëtan Gilbert
2019-09-24
Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopes
Matthieu Sozeau
2019-09-24
Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kind
Gaëtan Gilbert
2019-09-24
Make `zify` does work for `Z.to_N`
Kazuhiko Sakaguchi
2019-09-23
[macOS]immodules: *.so → *.dylib
Vincent Laporte
2019-09-23
[CI/Azure/macOS] Update GTK3 to 3.24.11
Vincent Laporte
2019-09-23
Fixes #10778 (fresh was not updated after renaming of intropattern entry in #...
Hugo Herbelin
2019-09-23
Merge PR #10776: Fix #10413 (CI failure on tags).
Gaëtan Gilbert
2019-09-23
Merge PR #10777: Mark SF as allow failure until it gets fixed.
Gaëtan Gilbert
2019-09-23
Mark SF as allow failure until it gets fixed.
Théo Zimmermann
2019-09-23
Fix #10413 (CI failure on tags).
Théo Zimmermann
2019-09-20
[ci] Add mit-pdos/perennial
Tej Chajed
2019-09-20
[ci] Remove OCaml "trunk" CI jobs.
Emilio Jesus Gallego Arias
2019-09-19
Fix #10420 Add dependent evar mapping info to output
Jim Fehrle
2019-09-19
Fix #10399: dependent evars line empty
Jim Fehrle
2019-09-19
[ci] Update supported OCaml version to 4.09.0
Emilio Jesus Gallego Arias
2019-09-19
[ocaml] Allow building with deprecated Obj primitives.
Emilio Jesus Gallego Arias
2019-09-18
[declaremods] Remove abstraction layer over module interpretation.
Emilio Jesus Gallego Arias
2019-09-18
[library] Move `Declaremods` to `vernac/`
Emilio Jesus Gallego Arias
2019-09-18
Fix syntax of reduction tactics when listing qualid to reduce or not.
Théo Zimmermann
2019-09-18
Merge PR #9856: A 'zify' tactic as a ML plugin
Maxime Dénès
2019-09-17
Merge PR #10738: update elpi to 1.7
Gaëtan Gilbert
2019-09-17
Merge PR #10476: Remove library-specific code for `Import`.
Enrico Tassi
2019-09-17
Add changelog entry
Maxime Dénès
2019-09-17
Overlay for VST
Maxime Dénès
2019-09-16
Fix #10757: Program Fixpoint uses "exists" for telescopes
Gaëtan Gilbert
2019-09-16
Define morphisms of real numbers and accelerate Cauchy reals
Vincent Semeria
2019-09-16
Re-implementation of zify
Frédéric Besson
2019-09-16
Optimize multiple imports
Maxime Dénès
2019-09-16
Optimize `Include`d `Export`s
Maxime Dénès
2019-09-16
Turn `module_objects` into a record
Maxime Dénès
2019-09-16
Add SF overlay
Maxime Dénès
2019-09-16
Optimize module Exports
Maxime Dénès
2019-09-16
Do not cache objects when importing modules
Maxime Dénès
2019-09-16
Specialize `ImportObject` to `Export`
Maxime Dénès
2019-09-16
`do_modtype` -> `load_modtype`
Maxime Dénès
2019-09-16
Remove library-specific code for `Import`.
Maxime Dénès
2019-09-13
Merge PR #10748: Hack for fixing #10578: handle between the three main CoqIDE...
Pierre-Marie Pédrot
2019-09-13
Hack for fixing #10578 (wrong initial handle position separating main windows).
Hugo Herbelin
2019-09-12
Merge PR #10753: Release notes for 8.10+beta3.
Clément Pit-Claudel
2019-09-12
Release notes for 8.10+beta3.
Théo Zimmermann
2019-09-11
Merge PR #8567: More general support for installation of coqide keys
Pierre-Marie Pédrot
2019-09-10
feat: Add a rewrite rule (UnderE) to unprotect evars in subgoals
Erik Martin-Dorel
2019-09-10
[ssr] Add test "do [under ... do ...] in H"
Erik Martin-Dorel
2019-09-10
Merge PR #10742: Switch maintenance of `ring` to a team
Théo Zimmermann
2019-09-10
Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely.
Hugo Herbelin
2019-09-10
Fixing coqide doc about location of "coqiderc" and "coqide.bindings".
Hugo Herbelin
2019-09-10
CoqIDE: removing option contextual menu on goal, inactive since 2da5db43c.
Hugo Herbelin
2019-09-10
Moving a standard string function (is_prefix) from Minilib to CString.
Hugo Herbelin
[prev]
[next]