aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-07-15Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc).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
2017-07-12Adding a comment regarding De Bruijn universe indices in the kernel.Pierre-Marie Pédrot
2017-07-11Remove deprecated options from ./configureThéo Zimmermann
2017-07-11Sync the manual with the deprecation warnings.Théo Zimmermann
2017-07-11[travis] Display info on tested commit for PR builds.Théo Zimmermann
2017-07-11Backtracking on deprecation of Bracketing Last Intro Pattern.Théo Zimmermann
2017-07-11Deprecate options that were introduced for compatibility with 8.5.Théo Zimmermann
2017-07-11Merge PR #871: Update Travis badge following the switch to masterMaxime Dénès
2017-07-11Update Travis badge following the switch to masterThéo Zimmermann
2017-07-11Moving the last bits of abtraction-breaking code out of the kernel.Pierre-Marie Pédrot
2017-07-11Fix nonsensical universe abstraction in the kernel.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the checker.Pierre-Marie Pédrot
2017-07-11Properly handling polymorphic inductive subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Cleaning up the implementation of module subtyping in the kernel.Pierre-Marie Pédrot
2017-07-11Safe API for accessing universe constraints of global references.Pierre-Marie Pédrot
2017-07-11Less footguns in universe handling: remove subst_instance_context.Pierre-Marie Pédrot
2017-07-11Asserting that monomorphic section variables have no abstracted context.Pierre-Marie Pédrot
2017-07-11Getting rid of simple calls to AUContext.instance.Pierre-Marie Pédrot
2017-07-11Merge branch 'v8.7'Maxime Dénès
2017-07-11Merge PR #858: [travis] Remove CompCert version check hack.Maxime Dénès
2017-07-11Merge PR #867: Removing a redundant universe instance information in native c...Maxime Dénès
2017-07-11Merge PR #860: use Int.equal instead of polymorphic =Maxime Dénès
2017-07-11Document the timing targetsJason Gross
2017-07-11Strip trailing spacesJason Gross
2017-07-11Add an entry to CHANGES about timing in coq_makefileJason Gross
2017-07-11Add timing scriptsJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 12:00:22 +0000