aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
...
* | 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
|\ \
| * | Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
| * | Assume totality: dedicated type rather than boolGravatar Arnaud Spiwack2016-06-14
* | | Univs: more robust Universe/Constraint decls #4816Gravatar Matthieu Sozeau2016-06-13
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\ \ \ | | |/ | |/|
* | | More informative error message when interpreting ltac variables in terms.Gravatar Pierre-Marie Pédrot2016-05-13
| * | Small optimization in evar resolution.Gravatar Pierre-Marie Pédrot2016-05-12
* | | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | | Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
| | * Revert "Prevent pretyping from checking well-guardedness unnecessarily."Gravatar Arnaud Spiwack2016-04-05
* | | Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* | | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | | Adding location to universes generated by the pretyper.Gravatar Pierre-Marie Pédrot2016-02-19
* | | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \ \
* | | | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| * | | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ / /
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\| |
| * | Fix bug #4519: oops, global shadowed local universe level bindings.Gravatar Matthieu Sozeau2016-01-23
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\| |
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\| |
| * | Fixing #4256 and #4484 (changes in evar-evar resolution made that newGravatar Hugo Herbelin2016-01-12
* | | mergeGravatar Matej Kosik2016-01-11
|\ \ \
| * | | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
|/ / /
* | | Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\| |
| * | Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-15
|\| |
| * | Fix bug #4293: ensure let-ins do not contain algebraic universes inGravatar Matthieu Sozeau2015-11-11
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\| |
| * | Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
* | | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-10-16
|\| |
| * | Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
| * | Fix #4346 2/2: VM casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
| * | Fix #4346 1/2: native casts were not inferring universe constraints.Gravatar Maxime Dénès2015-10-15
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-12
|\| |
| * | Refining 0c320e79ba30 in fixing interpretation of constr under bindersGravatar Hugo Herbelin2015-10-11
* | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\| |
| * | Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
| * | Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* | | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/ /
* | Univs (pretyping): call vm_compute/native_compute with the currentGravatar Matthieu Sozeau2015-10-06
* | Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
* | Univs (pretyping): allow parsing and decl of Top.nGravatar Matthieu Sozeau2015-10-02
| * Prevent pretyping from checking well-guardedness unnecessarily.Gravatar Arnaud Spiwack2015-09-25
* | Continuing 817308ab (use ltac env for terms in ltac context) + fixGravatar Hugo Herbelin2015-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 15:49:11 +0000