index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
Age
Commit message (
Expand
)
Author
2018-10-09
Refactoring of Micromega code using a Simplex linear solver
Frédéric Besson
2018-10-08
Merge PR #8668: Missing headers in two files
Théo Zimmermann
2018-10-08
Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.
Pierre-Marie Pédrot
2018-10-07
Adding missing header in functional_principles_types.ml.
Hugo Herbelin
2018-10-07
[api] Deprecate `evar_map` ref combinators.
Emilio Jesus Gallego Arias
2018-10-06
[api] Remove (most) 8.9 deprecated objects.
Emilio Jesus Gallego Arias
2018-10-05
[kernel] Remove section paths from `KerName.t`
Maxime Dénès
2018-10-04
Merge PR #8626: [ocaml] [lib] Remove some compatibility layers for OCaml < 4....
Pierre-Marie Pédrot
2018-10-02
Revert #6651: Use r.(p) syntax to print primitive projections
Maxime Dénès
2018-10-02
[ocaml] [lib] Remove some compatibility layers for OCaml < 4.03.0
Emilio Jesus Gallego Arias
2018-09-27
Merge PR #8570: [ssr] [camlp5] Remove warning from camlp5
Enrico Tassi
2018-09-27
Fixes #8553 (regression of tactic "change" under binders).
Hugo Herbelin
2018-09-27
[ssr] [camlp5] Remove warning from camlp5
Emilio Jesus Gallego Arias
2018-09-26
[print] Restrict use of "debug" Termops printer.
Emilio Jesus Gallego Arias
2018-09-26
Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)
Maxime Dénès
2018-09-26
Merge PR #8534: Checking if low-level name printers are used on purpose or not
Maxime Dénès
2018-09-25
Remove romega
Vincent Laporte
2018-09-24
[engine] Remove and deprecate `nf_enter` et al.
Emilio Jesus Gallego Arias
2018-09-24
Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.
Pierre-Marie Pédrot
2018-09-24
Merge PR #8464: Fix numeral notations
Hugo Herbelin
2018-09-23
[api] Deprecate constructors of deprecated datatypes.
Emilio Jesus Gallego Arias
2018-09-23
Merge PR #8465: Small cleanup of summary uses
Pierre-Marie Pédrot
2018-09-23
Checking if low-level name printers are used on purpose or not.
Hugo Herbelin
2018-09-21
Merge pull request #8462 from vbgl/zify-colonequal
Laurent Théry
2018-09-20
Merge PR #8297: Fix #7754: universe declarations on mutual inductives
Matthieu Sozeau
2018-09-19
Fix Numeral Notations (4/4 - fixing synch)
Jason Gross
2018-09-19
Fix Numeral Notations (3/4 - moving more stuff)
Jason Gross
2018-09-19
Fix Numeral Notations (2/4 - exceptions, usr_err)
Jason Gross
2018-09-19
Fix Numeral Notations (1/4 - moving things)
Jason Gross
2018-09-19
Merge PR #8246: Implementing an internal basic version of the "pose" tactic i...
Enrico Tassi
2018-09-19
[ssr] use the right environment in ssrpattern (fix #8454)
Enrico Tassi
2018-09-19
Fix #7754: universe declarations on mutual inductives
Gaëtan Gilbert
2018-09-19
Remove Hints.add_hints_init
Gaëtan Gilbert
2018-09-19
Merge PR #8447: Cleaning in the retroknowledge
Pierre-Marie Pédrot
2018-09-18
Zify: replace local definitions by equations
Vincent Laporte
2018-09-14
Merge PR #7894: Remove quote plugin
Théo Zimmermann
2018-09-14
Retroknowledge: use GlobRef.t instead of Constr.t as entry
Vincent Laporte
2018-09-14
Retroknowledge: simpler parsing rules
Vincent Laporte
2018-09-14
Retroknowledge: remove the (unused) by clause
Vincent Laporte
2018-09-14
Retroknowledge.KInt31: remove the (unused) group parameter
Vincent Laporte
2018-09-13
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Maxime Dénès
2018-09-13
Add explicit atribute for template polymorphism.
Gaëtan Gilbert
2018-09-12
Move maps & sets indexed by GlobRef.t into the kernel
Vincent Laporte
2018-09-12
Remove quote plugin
Maxime Dénès
2018-09-11
Merge PR #7288: Isolating ltac naming out of pretyping + fixing renaming
Pierre-Marie Pédrot
2018-09-11
Merge PR #8284: [ssr] anomaly -> error
Maxime Dénès
2018-09-11
Merge PR #8425: Deprecate romega in favor of lia
Pierre-Marie Pédrot
2018-09-10
Adapting standard library to the introduction of "Declare Scope".
Hugo Herbelin
2018-09-10
Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.
Hugo Herbelin
2018-09-10
Deprecate romega in favor of lia.
Vincent Laporte
[next]