index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
extraction
/
extraction.ml
Commit message (
Expand
)
Author
Age
*
Extraction: switch to EConstr.t as the central type to extract from.
Pierre Letouzey
2018-03-06
*
[api] Also deprecate constructors of Decl_kinds.
Emilio Jesus Gallego Arias
2017-12-23
*
Make some functions on terms more robust w.r.t new term constructs.
Maxime Dénès
2017-11-23
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
*
Efficient fresh name generation relying on sets.
Pierre-Marie Pédrot
2017-09-28
*
Merge PR #909: Extraction: reduce primitive projections in types (fix bug 4709)
Maxime Dénès
2017-08-01
|
\
|
*
Extraction: reduce primitive projections in types (fix bug 4709)
Pierre Letouzey
2017-07-26
*
|
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-07-26
|
/
*
[API] Remove `open API` in ml files in favor of `-open API` flag.
Emilio Jesus Gallego Arias
2017-07-17
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Remove (useless) aliases from the API.
Matej Košík
2017-06-10
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
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
2017-02-14
*
|
Cleaning up opening of the EConstr module in pretyping folder.
Pierre-Marie Pédrot
2017-02-14
*
|
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Retyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Reductionops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
*
|
Termops API using EConstr.
Pierre-Marie Pédrot
2017-02-14
|
*
Remove useless comments
Gaetan Gilbert
2017-01-28
|
*
Extend Fast_typeops to be a replacement for Typeops
Gaetan Gilbert
2016-12-12
|
/
*
Extraction: ignore some useless stuff about universes
Pierre Letouzey
2016-09-29
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
|
*
Fix typo.
Guillaume Melquiond
2016-06-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
|
|
*
Extraction : add a location in the error message about polyprop
Pierre Letouzey
2016-05-30
*
|
Extraction : add a location in the error message about polyprop
Pierre Letouzey
2016-05-30
|
*
Extraction/Projections: Fix bug #4710
Matthieu Sozeau
2016-05-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
Handle primitive projections inside types when extracting (bug #4616).
Guillaume Melquiond
2016-05-04
*
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
|
/
*
Extraction: more cautious use of intermediate result caching (fix #3923)
Pierre Letouzey
2015-12-15
*
Extraction: nicer implementation of Implicits
Pierre Letouzey
2015-12-12
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
Extraction: fix primitive projection extraction.
Matthieu Sozeau
2015-07-22
*
Update headers.
Maxime Dénès
2015-01-12
*
Extraction: no more ascii blob in type variables (fix #3227)
Pierre Letouzey
2015-01-11
*
Extraction : some more support functions for a future "Extraction Compute"
Pierre Letouzey
2015-01-11
*
Extraction: minor tweaks to ease ongoing experiments about Lambda
Pierre Letouzey
2015-01-11
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
[next]