aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
Commit message (Expand)AuthorAge
* Removing OCaml deprecated function names from the Lazy module.Gravatar Pierre-Marie Pédrot2016-03-10
* Renaming variants of Entries.local_entryGravatar Matej Kosik2016-02-16
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* | Renaming functions in Typing to stick to the standard e_* scheme.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
|\
| * Implement support for universe binder lists in Instance and Program Fixpoint/...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
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
|/
* Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
* Allow program hooks to see the refined universe_context at the end of aGravatar Matthieu Sozeau2015-11-19
* Command.declare_definition: grab the fix_exn early (follows 77cf18e)Gravatar Enrico Tassi2015-10-30
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Fix Definition id := Eval <redexpr> in by passing the right universeGravatar Matthieu Sozeau2015-10-12
* Axioms now support the universe binding syntax.Gravatar Pierre-Marie Pédrot2015-10-08
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Gravatar Hugo Herbelin2015-02-10
* Add the possibility of defining opaque terms with program.Gravatar mlasson2015-01-21
* Update headers.Gravatar Maxime Dénès2015-01-12
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* Fixing #3193 (honoring implicit arguments in local definitions).Gravatar Hugo Herbelin2014-10-03
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Fix categorization of recursive inductives.Gravatar Matthieu Sozeau2014-09-10
* Parsing of Type@{max(i,j)}.Gravatar Matthieu Sozeau2014-09-08
* Fixing bug #3492.Gravatar Pierre-Marie Pédrot2014-09-07
* Types declared as Variants really do not accept recursive definitions.Gravatar Arnaud Spiwack2014-09-04
* Simplify even further the declaration of primitive projections,Gravatar Matthieu Sozeau2014-08-30
* Fixing commit 50237af2.Gravatar Pierre-Marie Pédrot2014-08-29
* Fixing bug #3528.Gravatar Pierre-Marie Pédrot2014-08-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 00:40:08 +0000