index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
safe_typing.ml
Commit message (
Expand
)
Author
Age
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Using Maps to handle imports in Safe_typing. The order is irrelevant indeed,
Pierre-Marie Pédrot
2014-05-11
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Matthieu Sozeau
2014-05-06
*
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
Matthieu Sozeau
2014-05-06
*
Rework handling of universes on top of the STM, allowing for delayed
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing various backtrace recordings.
Pierre-Marie Pédrot
2014-04-25
*
Fix universe handling (bug introduced in vi2vo commit)
Enrico Tassi
2014-04-08
*
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-11
*
Fix (3243): univ constraints of module subtyping were not propagated
Enrico Tassi
2014-03-11
*
Using Hashmaps by default in constant and inductive maps. This changes fold and
Pierre-Marie Pédrot
2014-03-07
*
Using HMaps in Safe_env.environments, hopefully improving performances.
Pierre-Marie Pédrot
2014-03-05
*
STM: when batch compiling a vo, assert we behave conservatively
Enrico Tassi
2014-02-26
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
.vi files: .vo files without proofs
Enrico Tassi
2014-01-04
*
Remove obsolete comment about Let being processed synchronously
Enrico Tassi
2014-01-04
*
Removing native_name reference from constant_body.
Maxime Dénès
2013-12-28
*
STM: capture type checking error (Closes: 3195)
Enrico Tassi
2013-12-24
*
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-31
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
A shallow copy of a pre_env does not contain the vm cache
gareuselesinge
2013-10-03
*
ind_tables: properly handling side effects
gareuselesinge
2013-08-30
*
Remove Obj.magic from safe typing
gareuselesinge
2013-08-30
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Safe_typing code refactoring
letouzey
2013-08-20
*
get rid of closures in global/proof state
gareuselesinge
2013-08-08
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Safe_typing: minor factorisation
letouzey
2013-07-17
*
Added a Register Inline command for the native compiler. Will be ported to th...
mdenes
2013-07-10
*
Use definition_entry to declare local definitions
gareuselesinge
2013-05-09
*
Minor simplifications in Declaremods and Safe_typing
letouzey
2013-04-15
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Safe_typing+Libary: use some arrays instead of lists in vo structures
letouzey
2013-03-28
*
Safe_library : a record type for compiled_library instead of large tuple
letouzey
2013-03-28
*
Restrict (try...with...) to avoid catching critical exn (part 8)
letouzey
2013-03-13
*
Minor cleanup around Term_typing
letouzey
2013-02-27
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Slightly improving some debugging printing and error message for modules.
herbelin
2013-01-27
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
[next]