index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
engine
/
geninterp.ml
Age
Commit message (
Expand
)
Author
2017-11-21
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-03
Merge PR #6051: Fix FIXME: use OCaml 4.02 generative functors when available.
Maxime Dénès
2017-11-02
Exporting ValTMap for use in Genintern.
Hugo Herbelin
2017-11-01
Fix FIXME: use OCaml 4.02 generative functors when available.
Gaëtan Gilbert
2017-07-27
deprecate Pp.std_ppcmds type alias
Matej Košík
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-04
Normalizing the names of dynamic types to follow a typ_* scheme.
Pierre-Marie Pédrot
2016-05-04
Interpretation function can return any untyped value.
Pierre-Marie Pédrot
2016-05-04
Removing external uses of Val.inject and making Geninterp.interp return Val.t
Pierre-Marie Pédrot
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
Getting rid of the Geninterp.generic_interp function.
Pierre-Marie Pédrot
2016-05-04
Switching to an untyped toplevel representation for Ltac values.
Pierre-Marie Pédrot
2016-05-04
Moving Ftactic and Geninterp to the engine folder.
Pierre-Marie Pédrot
