aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Infering atomic ML entries from their grammar.Gravatar Pierre-Marie Pédrot2016-02-01
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fixing bug #3826: "Incompatible module types" is uninformative.Gravatar Pierre-Marie Pédrot2016-01-24
| * Fixing bug #4495: Failed assertion in metasyntax.ml.Gravatar Pierre-Marie Pédrot2016-01-24
| * Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
| * Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
* | Tactic notation printing accesses all the token data.Gravatar Pierre-Marie Pédrot2016-01-16
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
* | | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* | | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|\ \ \ | | |/ | |/|
* | | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
| |/ |/|
| * Inclusion of functors with restricted signature is now forbidden (fix #3746)Gravatar Pierre Letouzey2015-12-22
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...Gravatar Matej Kosik2015-12-18
* | CLEANUP: simplifying "Coqtop.init_gc" implementationGravatar Matej Kosik2015-12-18
* | CLEANUP: removing unnecessary wrapper functionGravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Print Assumptions: improve detection of case on an axiom of FalseGravatar Enrico Tassi2015-12-09
* | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* | Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Univs/Program: update the universe context with global universeGravatar Matthieu Sozeau2015-12-02
| * Fix bug #4444: Next Obligation performed after a Section opening wasGravatar Matthieu Sozeau2015-12-02
* | Removing dead code in Obligations.Gravatar Pierre-Marie Pédrot2015-12-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: correctly register universe binders for lemmas.Gravatar Matthieu Sozeau2015-11-28
| * Fix [Polymorphic Hint Rewrite].Gravatar Matthieu Sozeau2015-11-27
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
|\|
| * Univs: carry on universe substitution when defining obligations ofGravatar Matthieu Sozeau2015-11-24
| * Fix output of universe arcs. (Fix bug #4422)Gravatar Guillaume Melquiond2015-11-23
| * Univs: generation of induction schemes should not generated uselessGravatar Matthieu Sozeau2015-11-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
| * Allow program hooks to see the refined universe_context at the end of aGravatar Matthieu Sozeau2015-11-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 23:07:22 +0000