index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
extraction
Age
Commit message (
Expand
)
Author
2017-09-15
Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work...
Maxime Dénès
2017-08-29
Separating the module_type and module_body types by using a type parameter.
Pierre-Marie Pédrot
2017-08-21
Ensuring all .v files end with a newline to make "sed -i" work better on them.
Hugo Herbelin
2017-08-01
Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)
Maxime Dénès
2017-07-31
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Maxime Dénès
2017-07-28
Merge PR #889: Removing template polymorphism for definitions.
Maxime Dénès
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-26
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-25
[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-20
Extraction: fix bugs 5177 and 5240 (and also indirectly bug 4720)
Pierre Letouzey
2017-07-17
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-13
Remove the function Global.type_of_global_unsafe.
Pierre-Marie Pédrot
2017-07-05
Extraction TestCompile foo : a new command for extraction + ocamlc
Pierre Letouzey
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-14
Prelude : no more autoload of plugins extraction and recdef
Pierre Letouzey
2017-06-12
Merge PR#718: API cleanup: aliases
Maxime Dénès
2017-06-10
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-07
Put all plugins behind an "API".
Matej Kosik
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-05-30
Merge PR#692: Fail on deprecated warning even for Ocaml > 4.02.3
Maxime Dénès
2017-05-28
Fail on deprecated warning even for Ocaml > 4.02.3
Gaëtan Gilbert
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-25
Merge PR#481: [option] Remove support for non-synchronous options.
Maxime Dénès
2017-05-24
Merge branch 'trunk' into located_switch
Emilio Jesus Gallego Arias
2017-05-24
[option] Remove support for non-synchronous options.
Emilio Jesus Gallego Arias
2017-04-27
Fix omitted labels in function calls
Gaetan Gilbert
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-03-24
Merge branch 'trunk' into pr379
Maxime Dénès
2017-03-23
Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."
Maxime Dénès
2017-03-23
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-03-23
Add empty Extraction.v and FunInd.v to prepare landing of PR#220.
Maxime Dénès
2017-03-21
[extraction] Flush formatters at end of output.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Make feedback the only logging mechanism.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Prepare for serialization, remove opaque glue.
Emilio Jesus Gallego Arias
2017-03-21
[pp] Remove `Pp.stras`.
Emilio Jesus Gallego Arias
2017-03-14
[safe-string] plugins/extraction
Emilio Jesus Gallego Arias
2017-02-17
Moving the Ltac plugin to a pack-based one.
Pierre-Marie Pédrot
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Definining EConstr-based contexts.
Pierre-Marie Pédrot
2017-02-14
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
Reductionops now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
Eliminating parts of the right-hand side compatibility layer
Pierre-Marie Pédrot
2017-02-14
Inv API using EConstr.
Pierre-Marie Pédrot
[next]