index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
Commit message (
Expand
)
Author
Age
...
|
*
|
|
|
|
Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).
Hugo Herbelin
2017-11-20
*
|
|
|
|
|
Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.
Maxime Dénès
2017-11-20
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6161: Fix micromega.ml to match generated file and enforce match in...
Maxime Dénès
2017-11-20
|
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
Fix #5790: make Hint Resolve <- respect univ polymorphism flag.
Gaëtan Gilbert
2017-11-19
|
|
_
|
_
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
|
|
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
2017-11-19
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
[proof] Attempt to deprecate some V82 parts of the proof API.
Emilio Jesus Gallego Arias
2017-11-19
|
|
_
|
/
/
/
|
/
|
|
|
|
*
|
|
|
|
Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.
Maxime Dénès
2017-11-16
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2
Maxime Dénès
2017-11-16
|
\
\
\
\
\
\
|
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
*
|
|
Fix micromega.ml to match generated file and enforce match in make.
Gaëtan Gilbert
2017-11-16
|
|
_
|
/
/
/
|
/
|
|
|
|
|
|
|
*
|
Fixing printing of tactics encapsulated as tacarg with Tacexp.
Hugo Herbelin
2017-11-15
|
|
|
*
|
Using "l" printer for glob_constr, like for constr.
Hugo Herbelin
2017-11-15
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Maxime Dénès
2017-11-13
|
\
\
\
|
|
|
*
ssr: fill_occ_pattern: return valid ustate even if no match (fix #6106)
Enrico Tassi
2017-11-09
|
*
|
|
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
|
|
|
/
|
|
/
|
*
/
|
Adding support for syntax "let _ := e in e'" in Ltac.
Hugo Herbelin
2017-11-04
|
/
/
*
|
Merge PR #6047: A generic printer for ltac values
Maxime Dénès
2017-11-03
|
\
\
*
\
\
Merge PR #6021: Fixing #2881 ("change with" failing in an Ltac definition).
Maxime Dénès
2017-11-03
|
\
\
\
|
|
*
|
Ltac Debug: exporting env and sigma when needed so that term can be printed.
Hugo Herbelin
2017-11-02
|
|
*
|
Binding ltac printing functions to the system of generic printing.
Hugo Herbelin
2017-11-02
|
|
*
|
Setting a system to register printers for Ltac values.
Hugo Herbelin
2017-11-02
|
|
*
|
Using a specific function to register vernac printers.
Hugo Herbelin
2017-11-02
|
|
*
|
Exporting a few more printing functions.
Hugo Herbelin
2017-11-02
|
|
*
|
Improving checks about the list separator in tactic notations.
Hugo Herbelin
2017-11-02
|
|
/
/
|
/
|
|
|
*
|
Fixing #2881 ("change with" failing in an Ltac definition).
Hugo Herbelin
2017-10-30
*
|
|
Merge PR #6015: [general] Remove Econstr dependency from `intf`
Maxime Dénès
2017-10-27
|
\
\
\
*
\
\
\
Merge PR #677: Trunk+abstracting injection flags
Maxime Dénès
2017-10-27
|
\
\
\
\
|
|
_
|
/
/
|
/
|
|
|
|
*
|
|
Passing around the flag for injection so that tactics calling inj at
Hugo Herbelin
2017-10-26
|
|
|
*
Use GHC.Base.Any for compatibility with GHC 8.2
Tej Chajed
2017-10-25
|
|
_
|
/
|
/
|
|
|
|
*
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
|
|
/
*
/
Typo in comment in tactic_matching.ml.
Hugo Herbelin
2017-10-24
|
/
*
Merge PR #1095: [stm] Remove state handling from Futures
Maxime Dénès
2017-10-20
|
\
*
|
Moving bug numbers to BZ# format in the source code.
Théo Zimmermann
2017-10-19
|
*
[stm] Remove state-handling from Futures.
Emilio Jesus Gallego Arias
2017-10-17
|
/
*
[stdlib] Fix warnings on deprecated `Add Setoid`
Emilio Jesus Gallego Arias
2017-10-15
*
[vernac] Remove "Proof using" hacks from parser.
Emilio Jesus Gallego Arias
2017-10-10
*
Merge PR #768: Omega and romega know about context definitions (fix old bug 148)
Maxime Dénès
2017-10-10
|
\
*
\
Merge PR #1087: [stm] Switch to a functional API
Maxime Dénès
2017-10-09
|
\
\
*
\
\
Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...
Maxime Dénès
2017-10-09
|
\
\
\
*
\
\
\
Merge PR #1114: Generic handling of nameable objects for plugins
Maxime Dénès
2017-10-09
|
\
\
\
\
|
|
|
*
|
[stm] Switch to a functional API
Emilio Jesus Gallego Arias
2017-10-06
|
|
_
|
/
/
|
/
|
|
|
*
|
|
|
Merge PR #1118: Extraction : minor support stuff for the new Extraction Compu...
Maxime Dénès
2017-10-06
|
\
\
\
\
|
|
|
*
|
[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.
Emilio Jesus Gallego Arias
2017-10-05
|
|
|
|
*
romega: takes advantage of context variables with body
Pierre Letouzey
2017-10-05
|
|
|
|
*
Omega now aware of context variables with bodies (in type Z or nat) (fix bug ...
Pierre Letouzey
2017-10-05
|
|
|
|
/
*
|
|
/
Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...
Pierre Letouzey
2017-10-05
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #1006: fix: ssrmatching and primitive projections
Maxime Dénès
2017-10-04
|
\
\
\
*
\
\
\
Merge PR #1078: Report missing arguments in error message
Maxime Dénès
2017-10-04
|
\
\
\
\
|
|
|
*
|
Extraction : minor support stuff for the new Extraction Compute plugin
Pierre Letouzey
2017-10-04
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
Ltac uses the new generic locatable API.
Pierre-Marie Pédrot
2017-10-03
[prev]
[next]