aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
* 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
* 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
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 06:04:18 +0000