aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
...
| * Do not typecheck twice the type of opaque constants.Gravatar Maxime Dénès2017-03-21
* | Merge PR#134: Enable `-safe-string`Gravatar Maxime Dénès2017-03-21
|\ \
| * | [safe_string] kernel/term_typingGravatar Emilio Jesus Gallego Arias2017-03-14
* | | [future] Remove unused parameter greedy.Gravatar Emilio Jesus Gallego Arias2017-03-14
|/ /
* | Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Gravatar Matej Kosik2016-08-25
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Adding a local type-in-type flag in kernel declarations.Gravatar Pierre-Marie Pédrot2016-06-18
* Factorizing the uses of Declareops.safe_flags.Gravatar Pierre-Marie Pédrot2016-06-16
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 02:40:34 +0000