aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Refine Gregory Malecha's patch on VM and universe polymorphism.Gravatar Maxime Dénès2015-10-28
* Conversion of polymorphic inductive types was incomplete in VM and native.Gravatar Maxime Dénès2015-10-28
* Fix minor typo in native compiler.Gravatar Maxime Dénès2015-10-28
* test cases.Gravatar Gregory Malecha2015-10-28
* Adds support for the virtual machine to perform reduction of universe polymor...Gravatar Gregory Malecha2015-10-28
* Univs: fix bug #4375, accept universe binders on (co)-fixpointsGravatar Matthieu Sozeau2015-10-28
* Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"Gravatar Hugo Herbelin2015-10-28
* Seeing configure as a static resolution of path continued (not yet on windows).Gravatar Hugo Herbelin2015-10-28
* Do not pause globing in funind. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-28
* Fix bugs 4389, 4390 and 4391 due to wrong handling of universe namesGravatar Matthieu Sozeau2015-10-27
* Seeing configure as a static resolution of path, hence hardwiring longGravatar Hugo Herbelin2015-10-26
* Fixing bugs in options of the configure.Gravatar Hugo Herbelin2015-10-26
* Preventing using OCaml 4.02.0 for compiling Coq as compilation timesGravatar Hugo Herbelin2015-10-26
* Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
* Preserving goal name in revert/bring_hyps.Gravatar Hugo Herbelin2015-10-26
* Two test-suite files for bugs 3974 and 3975Gravatar Pierre Letouzey2015-10-26
* Declaremods: replace two anomalies by user errors (fix #3974 and #3975)Gravatar Pierre Letouzey2015-10-25
* Safe_typing: add clean_bounded_mod_expr in Include Self of modtype (fix #4331)Gravatar Pierre Letouzey2015-10-25
* Minor module cleanup : error HigherOrderInclude was never happeningGravatar Pierre Letouzey2015-10-25
* Fixing a loop in checking hints with holes.Gravatar Hugo Herbelin2015-10-24
* Backtracking on interpreting toplevel calls to exact in scope determinedGravatar Hugo Herbelin2015-10-24
* Support "Functional Scheme" in coqdoc. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-23
* Fixing a bug in reporting ill-formed inductive.Gravatar Hugo Herbelin2015-10-22
* Mention bug 3199 fix as a source of incompatibilities.Gravatar Matthieu Sozeau2015-10-21
* Bug #3956 is fixed.Gravatar Matthieu Sozeau2015-10-21
* Fixed (and changed) infoH.Gravatar Pierre Courtieu2015-10-21
* Fix lemma-overloadingGravatar Matthieu Sozeau2015-10-20
* Do occur-check w.r.t existential's types also when instantiating an evar.Gravatar Matthieu Sozeau2015-10-19
* Categorizing debug messages as such + NonLogical uses loggers.Gravatar Pierre Courtieu2015-10-19
* Test for #4372 (anomaly in inversion in the presence of fake dependency).Gravatar Hugo Herbelin2015-10-19
* Turning anomaly into error for #4372 (weakness of inversion in theGravatar Hugo Herbelin2015-10-19
* Partly fixes #3225. Removed some old experimental stuff in funind.Gravatar Pierre Courtieu2015-10-19
* Fixed #4274, bad formatting of messages in emacs mode.Gravatar Pierre Courtieu2015-10-19
* Documenting the option "Strict Universe Declaration" in CHANGES.Gravatar Pierre-Marie Pédrot2015-10-19
* Miscellaneous typos, spacing, US spelling in comments or variable names.Gravatar Hugo Herbelin2015-10-18
* Using "__" rather than this unelegant arbitrary "A" for the name of variables...Gravatar Hugo Herbelin2015-10-18
* Reference Manual: Applying standard style recommendation about notGravatar Hugo Herbelin2015-10-18
* Fixing #4198 (continued): not matching within the inner lambdas/let-insGravatar Hugo Herbelin2015-10-18
* Using appropriate lambda decomposition function counting let-ins whenGravatar Hugo Herbelin2015-10-18
* Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Gravatar Hugo Herbelin2015-10-18
* Lemmas accept the Local flag.Gravatar Pierre-Marie Pédrot2015-10-17
* Test for bug #4325.Gravatar Pierre-Marie Pédrot2015-10-17
* Generalize fix for auto from PMP to eauto and typeclasses eauto.Gravatar Matthieu Sozeau2015-10-16
* Remove left2right reference from the kernel.Gravatar Maxime Dénès2015-10-16
* Merge hint lists instead of appending them. (Fix bug #3199)Gravatar Guillaume Melquiond2015-10-16
* Avoid dependency of the pretyper on C code.Gravatar Maxime Dénès2015-10-15
* Test file for #4346: Set is no longer of type TypeGravatar 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
* Warn user when bytecode compilation fails.Gravatar Maxime Dénès2015-10-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 18:04:55 +0000