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
*
Fix typo.
Guillaume Melquiond
2016-06-23
*
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
*
Handle primitive projections inside types when extracting (bug #4616).
Guillaume Melquiond
2016-05-04
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
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
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
instanciation is French, instantiation is English
Jason Gross
2014-08-25
*
A tentative uniform naming policy in module Inductiveops.
Hugo Herbelin
2014-08-01
*
Reuse universe level substitutions for template polymorphism, fixing performance
Matthieu Sozeau
2014-05-09
*
Fix extraction taking a type in the wrong environment.
Matthieu Sozeau
2014-05-06
*
Fix a pervasive equality use.
Matthieu Sozeau
2014-05-06
*
- Rename eq to equal in Univ, document new modules, set interfaces.
Matthieu Sozeau
2014-05-06
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing Pervasives.equality in extraction.
Pierre-Marie Pédrot
2014-03-03
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Restrict (try...with...) to avoid catching critical exn (part 9)
letouzey
2013-03-13
*
Restrict (try...with...) to avoid catching critical exn (part 6)
letouzey
2013-03-13
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Extraction: same as commit 16203, hopefully without NotASort exns
letouzey
2013-02-18
*
Fix extraction of inductive types that Coq auto-detects to be in Prop
letouzey
2013-02-14
*
Modulification of Label
ppedrot
2012-12-18
*
Extraction of projections: restrict a hack to ocaml only (fix #2941)
letouzey
2012-12-17
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
Extraction Implicit: consider the parameters of a constructor (fix #2905)
letouzey
2012-10-30
*
Cleaning interface of Util.
ppedrot
2012-09-18
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
[next]