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