aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term_typing.ml
Commit message (Expand)AuthorAge
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Unify pre_env and envGravatar Maxime Dénès2018-05-28
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [nit] Remove some unnecessary global `open Feedback`Gravatar Emilio Jesus Gallego Arias2018-02-09
* Enforce that polymorphic definitions do not generate internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
* Returning instance instead of substitution in universe context abstraction.Gravatar Pierre-Marie Pédrot2017-12-30
* Let definitions do not create new universe constraints.Gravatar Pierre-Marie Pédrot2017-12-19
* Specific type for section definition entries.Gravatar Pierre-Marie Pédrot2017-12-19
* Let definitions must not contain side-effects when reaching the kernel.Gravatar Pierre-Marie Pédrot2017-12-16
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* [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
|\ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 06:18:05 +0000