aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/declareops.ml
Commit message (Expand)AuthorAge
...
* Declareops + Modops : more clever substitutionsGravatar letouzey2013-08-20
* Attempt to restore hash-consing of opaque termsGravatar letouzey2013-08-20
* abstract+Defined: create opaque sub proofs (as pre-ParalITP)Gravatar gareuselesinge2013-08-19
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26