aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-19[proofs] Remove circular dependency from Proofview to Goal.Emilio Jesus Gallego Arias
2017-07-19[general] Move files to directories matching linking order.Emilio Jesus Gallego Arias
2017-07-19Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.Maxime Dénès
2017-07-19[pp] Fix bugs 5651 [incorrect thunk in pretty printer]Emilio Jesus Gallego Arias
2017-07-19Fix debug trace of typeclasses eauto.Théo Zimmermann
2017-07-19Fixing the checker w.r.t. wrongly used abstract universe contexts.Pierre-Marie Pédrot
2017-07-19Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true.Maxime Dénès
2017-07-18Improve do_split option of typeclass resolutionMatthieu Sozeau
2017-07-18[ci] VST is now built with IGNORECOQVERSION=true.Théo Zimmermann
2017-07-18Fixing a little location bug with recursive binders.Hugo Herbelin
2017-07-17Merge PR #781: Remove dead code [Universes.simplify_universe_context]Maxime Dénès
2017-07-17Merge PR #783: Remove some useless code in Term_typingMaxime Dénès
2017-07-17Merge PR #822: [meta] [api] Fix META file for API introduction.Maxime Dénès
2017-07-17[funind] Remove spurious character in comment.Emilio Jesus Gallego Arias
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
2017-07-17[meta] [api] Fix META file for API introduction.Emilio Jesus Gallego Arias
2017-07-17Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layersMaxime Dénès
2017-07-17Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body move...Maxime Dénès
2017-07-17Merge PR #879: Adding debug printers related to universesMaxime Dénès
2017-07-17Merge PR #874: Adding econstr printer to "include" file.Maxime Dénès
2017-07-17Merge PR #872: [travis] Display info on tested commit for PR builds.Maxime Dénès
2017-07-17Merge PR #865: RefMan-ext: fix some typosMaxime Dénès
2017-07-17Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat...Maxime Dénès
2017-07-17Merge PR #861: Fix typo in documentation for identityMaxime Dénès
2017-07-16Removing a dummy parameter in some FMapPositive statements.Hugo Herbelin
2017-07-16Adapting to 91df40272 (body_of_constant_body moved to global).Hugo Herbelin
2017-07-14Update with non structurally recursivewilliam-lawvere
2017-07-14Adding debug printers related to universes in the default debugger source file.Pierre-Marie Pédrot
2017-07-14Fix a typo in dev/changes.Pierre-Marie Pédrot
2017-07-14Document the changes in API brought by this series of patches.Pierre-Marie Pédrot
2017-07-14Getting rid of abstraction breaking code in tclABSTRACT.Pierre-Marie Pédrot
2017-07-13[travis] Update testing to 4.05.0 + Camlp5 7.01Emilio Jesus Gallego Arias
2017-07-13Removing a use of AUContext.instance in the STM.Pierre-Marie Pédrot
2017-07-13Removing the uses of abstraction-breaking code in Lemmas.Pierre-Marie Pédrot
2017-07-13Set version to 8.7+alpha.Maxime Dénès
2017-07-13Removing the uses of abstraction-breaking code in Obligations.Pierre-Marie Pédrot
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
2017-07-13The only abstraction-breaking function in Univ is now AUContext.instance.Pierre-Marie Pédrot
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Elimschemes.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Discharge.Pierre-Marie Pédrot
2017-07-13Make the typeclass implementation fully compatible with universe polymorphism.Pierre-Marie Pédrot
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-13Safer API for Global.type_of_global_in_context.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Record.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Search.Pierre-Marie Pédrot
2017-07-13Getting rid of AUContext abstraction breakers in Recordops.Pierre-Marie Pédrot
2017-07-13Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: KernelMaxime Dénès
2017-07-12Adding econstr printer to "include" file.Hugo Herbelin
2017-07-12format pairs of items for pr_depth to get alternating separatorsPaul Steckler
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 15:02:41 +0000