index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
safe_typing.ml
Age
Commit message (
Expand
)
Author
2019-12-07
Section.t is never empty
Gaëtan Gilbert
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-11-01
Implement classify on primitive float
Pierre Roux
2019-11-01
Change return type of primitive float comparison
Pierre Roux
2019-11-01
Add primitive float computation in Coq kernel
Guillaume Bertholon
2019-11-01
Declare type of primitives in CPrimitives
Pierre Roux
2019-10-24
Raise an anomaly when looking up unknown constant/inductive
Gaëtan Gilbert
2019-10-23
Merge PR #10884: Last stop before CEP 40
Maxime Dénès
2019-10-19
universes_of_private: return set instead of list of sets
Gaëtan Gilbert
2019-10-16
Ensure that side-effect declarations reaching the kernel are forced.
Pierre-Marie Pédrot
2019-10-16
Split the function used to declare side-effects from the standard one.
Pierre-Marie Pédrot
2019-10-16
Cleaning up the previous code by ensuring statically invariants on opaque pro...
Pierre-Marie Pédrot
2019-10-16
Make explicit the delayed computation of opaque bodies in Term_typing.
Pierre-Marie Pédrot
2019-10-14
Remove [in_section] arguments to Safe_typing functions
Gaëtan Gilbert
2019-10-12
Merge PR #10818: Merge Direct and Indirect nodes in Opaqueproof.
Maxime Dénès
2019-10-04
Merge Direct and Indirect nodes in Opaqueproof.
Pierre-Marie Pédrot
2019-10-04
Remove redundancy in section hypotheses of kernel entries.
Pierre-Marie Pédrot
2019-10-02
Loosen restrictions on mixing universe mono/polymorphism in sections
Gaëtan Gilbert
2019-09-26
Move the declararation of delayed constraints out of add_constant_aux.
Pierre-Marie Pédrot
2019-09-26
Implement section discharging inside kernel.
Pierre-Marie Pédrot
2019-09-25
Move the Lib section data into the kernel.
Pierre-Marie Pédrot
2019-09-25
Stub code for handling sections in kernel.
Pierre-Marie Pédrot
2019-08-16
Set/Unset commands for typing flags
SimonBoulier
2019-07-08
Similar purity invariants in the kernel.
Pierre-Marie Pédrot
2019-07-04
Merge PR #10461: Simplify Declare.declare_variable
Emilio Jesus Gallego Arias
2019-07-04
Merge PR #10359: Remove dependency of native_compile on global env for symbols
Maxime Dénès
2019-07-03
Safe_typing.push_named_assum: don't take universes
Gaëtan Gilbert
2019-06-27
Kernel transparent definition entries have no body universes.
Gaëtan Gilbert
2019-06-26
Perform the opaque section variable inference outside of the kernel.
Pierre-Marie Pédrot
2019-06-24
Remove the unused opaque_entry_inline_code field from opaque entries.
Pierre-Marie Pédrot
2019-06-24
Enforce that opaque entries carry their type.
Pierre-Marie Pédrot
2019-06-24
Dedicated type for opaque entries in the kernel.
Pierre-Marie Pédrot
2019-06-24
Enforce that transparent entries are forced beforehand.
Pierre-Marie Pédrot
2019-06-24
Take advantage of the change of entry representation to split opacity status.
Pierre-Marie Pédrot
2019-06-17
Merge PR #10362: Kernel-side delaying of polymorphic opaque constants
Gaëtan Gilbert
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-17
Clean up the code adding monomorphic global constraints in Safe_typing.
Pierre-Marie Pédrot
2019-06-17
Merge universe quantification and delayed constraints in opaque proofs.
Pierre-Marie Pédrot
2019-06-17
Allow to delay polymorphic opaque constants.
Pierre-Marie Pédrot
2019-06-12
Remove dependency of native_compile on global env for symbols
Gaëtan Gilbert
2019-06-11
Remove the side-effect role from the kernel.
Pierre-Marie Pédrot
2019-06-11
Move type definition Nativecode.symbols to Nativevalues
Gaëtan Gilbert
2019-06-06
Merge the two sources of monomorphic constraints for side-effects.
Pierre-Marie Pédrot
2019-06-04
Do not substitute opaque constants when discharging.
Pierre-Marie Pédrot
2019-05-27
Merge PR #10249: More precise type for export and inlining of private constants
Maxime Dénès
2019-05-26
More precise type for Safe_typing export and inlining of private constants.
Pierre-Marie Pédrot
2019-05-25
Centralize the hashconsing of constant declarations.
Pierre-Marie Pédrot
2019-05-24
Remove a last use of opacity-piercing function in Safe_typing.
Pierre-Marie Pédrot
2019-05-20
Ensure statically that declarations built by Term_typing are direct.
Pierre-Marie Pédrot
2019-05-19
Parameterize the constant_body type by opaque subproofs.
Pierre-Marie Pédrot
[next]
