index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
extraction
Commit message (
Expand
)
Author
Age
*
[ssreflect] Fix module scoping problems due to packing and mli files.
Emilio Jesus Gallego Arias
2018-03-10
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...
Maxime Dénès
2018-03-08
|
\
|
*
An experimental 'Show Extraction' command (grant feature wish #4129)
Pierre Letouzey
2018-03-06
|
*
Extraction: switch to EConstr.t as the central type to extract from.
Pierre Letouzey
2018-03-06
*
|
[stdlib] Do not use deprecated notations
Vincent Laporte
2018-03-06
*
|
Update headers following #6543.
Théo Zimmermann
2018-02-27
|
/
*
Change references to CAMLP4 to CAMLP5 to be more accurate since we no
Jim Fehrle
2018-02-17
*
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
*
issue deprecation warning for "Ocaml"
Paul Steckler
2017-12-06
*
use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language
Paul Steckler
2017-12-05
*
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Maxime Dénès
2017-12-05
|
\
|
*
allow :: and , as infix ops
Paul Steckler
2017-11-27
*
|
Merge PR #486: Make some functions on terms more robust w.r.t new term constr...
Maxime Dénès
2017-11-24
|
\
\
|
*
|
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-23
|
|
*
allow whitespace around infix op
Paul Steckler
2017-11-22
|
|
*
use OCaml criteria for infix ops, #6212
Paul Steckler
2017-11-22
|
|
/
*
/
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
|
/
*
Merge PR #6023: Use GHC.Base.Any for compatibility with GHC 8.2
Maxime Dénès
2017-11-16
|
\
*
|
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
|
*
Use GHC.Base.Any for compatibility with GHC 8.2
Tej Chajed
2017-10-25
|
/
*
Moving bug numbers to BZ# format in the source code.
Théo Zimmermann
2017-10-19
*
Merge PR #1118: Extraction : minor support stuff for the new Extraction Compu...
Maxime Dénès
2017-10-06
|
\
*
|
Extraction: reduce eta-redexes whose cores are atomic (solves indirectly BZ#4...
Pierre Letouzey
2017-10-05
|
*
Extraction : minor support stuff for the new Extraction Compute plugin
Pierre Letouzey
2017-10-04
|
/
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...
Maxime Dénès
2017-09-15
|
\
*
|
Separating the module_type and module_body types by using a type parameter.
Pierre-Marie Pédrot
2017-08-29
|
*
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-21
|
/
*
Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)
Maxime Dénès
2017-08-01
|
\
*
\
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-31
|
\
\
*
\
\
Merge PR #889: Removing template polymorphism for definitions.
Maxime Dénès
2017-07-28
|
\
\
\
|
|
*
|
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-27
|
|
|
*
Extraction: reduce primitive projections in types (fix bug 4709)
Pierre Letouzey
2017-07-26
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #918: Extraction: do not mix Haskell types Any and () (fix bugs 4844...
Maxime Dénès
2017-07-26
|
\
\
\
|
|
_
|
/
|
/
|
|
|
|
*
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
|
|
/
|
/
|
*
|
Merge PR #905: [api] Remove type equalities from API.
Maxime Dénès
2017-07-26
|
\
\
*
\
\
Merge PR #857: Extraction: various fixes related with bug 4720
Maxime Dénès
2017-07-26
|
\
\
\
*
\
\
\
Merge PR #859: Extraction TestCompile
Maxime Dénès
2017-07-26
|
\
\
\
\
|
|
|
*
|
[api] Remove type equalities from API.
Emilio Jesus Gallego Arias
2017-07-25
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
Extraction: do not mix Haskell types Any and () (revert 8e257d4, fix bugs 484...
Pierre Letouzey
2017-07-25
|
|
_
|
/
|
/
|
|
|
|
*
Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)
Pierre Letouzey
2017-07-20
|
|
/
|
/
|
*
|
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
|
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-13
|
*
Extraction TestCompile foo : a new command for extraction + ocamlc
Pierre Letouzey
2017-07-05
|
/
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-14
*
Merge PR#718: API cleanup: aliases
Maxime Dénès
2017-06-12
|
\
*
|
Remove remaining vo.itarget files (obsolete since PR #499)
Pierre Letouzey
2017-06-10
|
*
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
|
/
[next]