aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
* Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\
| * [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | Merge PR#537: Efficient side-effect abstractionGravatar Maxime Dénès2017-04-11
|\ \ | |/ |/|
* | Inline the only use of hcons_j in Term_typing.Gravatar Pierre-Marie Pédrot2017-04-07
* | Documenting the fact terms are only hashconsed outside of a section.Gravatar Pierre-Marie Pédrot2017-04-06
| * Fix substitution of abstracted lemmas.Gravatar Pierre-Marie Pédrot2017-04-04
* | More efficient check in validity of side-effects.Gravatar Pierre-Marie Pédrot2017-03-27
* | Fix hashconsing of terms in the kernel.Gravatar Pierre-Marie Pédrot2017-03-27
|/
* Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-24
|\
| * Using a dedicated datastructure for side effect ordering.Gravatar Pierre-Marie Pédrot2017-03-23
| * Making the side_effects type opaque.Gravatar Pierre-Marie Pédrot2017-03-23
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\|
| * Add a few comments in term_typing.ml.Gravatar Maxime Dénès2017-03-21
| * 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
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 13:56:21 +0000