aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Take Suggest Proof Using outside the kernel.Gravatar Gaëtan Gilbert2017-10-10
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Avoiding a variable shadowing in the kernel.Gravatar Pierre-Marie Pédrot2017-07-26
* Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Further simplication: do not recreate entries for side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* More precise type of entries capturing their lack of side-effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Using a record type for Cooking.result.Gravatar Pierre-Marie Pédrot2017-07-26
* More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
* Merge PR #783: Remove some useless code in Term_typingGravatar Maxime Dénès2017-07-17
|\
* | Fix nonsensical universe abstraction in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* | Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* | Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* | Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| * Remove some useless code in Term_typingGravatar Gaëtan Gilbert2017-06-13
* | [kernel] Improve proof using message, fixes bugzilla #3613Gravatar Emilio Jesus Gallego Arias2017-06-07
|/
* 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
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-18 20:57:49 +0000