aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
...
| * Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\ \
| * | Rename Ephemeron -> CEphemeron.Gravatar Maxime Dénès2016-03-04
* | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \ | |/ / |/| |
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Fix handling of side-effects in case of `Opaque side-effects as well.Gravatar Matthieu Sozeau2016-01-04
* | | Fix bug #4456, anomaly in handle-side effectsGravatar Matthieu Sozeau2015-12-31
|/ /
* | Cleanup API and comments of 908dcd613Gravatar Enrico Tassi2015-10-29
* | Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* | Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* | Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* | term_typing: strengthen discharging codeGravatar Enrico Tassi2015-10-08
* | Univs: handle side-effects of futures correctly in kernel.Gravatar Matthieu Sozeau2015-10-02
* | Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
| * Add a field in `constant_body` to track constant whose well-foundedness is as...Gravatar Arnaud Spiwack2015-09-25
| * Propagate `Guarded` flag from syntax to kernel.Gravatar Arnaud Spiwack2015-09-25
* | Fix handling of primitive projections in VM.Gravatar Maxime Dénès2015-07-05
|/
* Fix vm compiler to refuse to compile code making use of inductives withGravatar Matthieu Sozeau2015-03-25
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Univs: Fix alias computation for VMs, computation of normal form ofGravatar Matthieu Sozeau2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Exporting the function handling side-effects only applied to terms.Gravatar Pierre-Marie Pédrot2014-11-20
* Slightly improving error messages when mismatch with Proof using at Qed time.Gravatar Hugo Herbelin2014-11-19
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Change the way primitive projections are declared to the kernel.Gravatar Matthieu Sozeau2014-08-28
* make a few lines fit the screenGravatar Enrico Tassi2014-08-05
* - Fix handling of opaque polymorphic definitions which were turned transparent.Gravatar Matthieu Sozeau2014-08-03
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-21
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
* Fix a de Bruijn bug in checking code of projections.Gravatar Matthieu Sozeau2014-06-17
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* ind_tables: always declare side effects (Closes: HOTT#110)Gravatar Enrico Tassi2014-06-08
* - Fix eq_constr_universes restricted to Sorts.equalGravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* Various fixes of universe polymorphism and projections when they're set.Gravatar Matthieu Sozeau2014-05-06
* - Fix Check to use the constraints inferred during type inference.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 23:27:47 +0000