| Commit message (Expand) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | | | | | | | | | | | | | | Merge PR #896: Prepare De Bruijn universe abstractions, Spin-off: Checker |  Maxime Dénès | 2017-07-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #869: Enforce alternating separators in typeclass debug output | Maxime Dénès | 2017-07-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #877: Travis+4.05.0 | Maxime Dénès | 2017-07-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | Merge branch 'v8.7' | Maxime Dénès | 2017-07-20 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | | Merge PR #745: Add timing scripts | Maxime Dénès | 2017-07-19 | |
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #855: Deprecate options that were introduced for compatibility with ... | Maxime Dénès | 2017-07-19 | |
| | |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | 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-19 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | | Merge 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-19 | |
| | |_|_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | * | | | | Fix debug trace of typeclasses eauto. |  Théo Zimmermann | 2017-07-19 | |
| | | | | | | | | * | | | | | | | | | Fixing the checker w.r.t. wrongly used abstract universe contexts. |  Pierre-Marie Pédrot | 2017-07-19 | |
| | | | | | | | | | |_|_|_|/ / / / | | | | | | | | |/| | | | | | | | ||||
| * | | | | | | | | | | | | | | | | Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true. | Maxime Dénès | 2017-07-19 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| | | | | | | | | | * | | | | | | | Improve do_split option of typeclass resolution |  Matthieu Sozeau | 2017-07-18 | |
| | |_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | ||||
| | * | | | | | | | | | | | | | | [ci] VST is now built with IGNORECOQVERSION=true. | Théo Zimmermann | 2017-07-18 | |
| |/ / / / / / / / / / / / / / | ||||
| | | | | | | | | | | | | * | | Fixing a little location bug with recursive binders. |  Hugo Herbelin | 2017-07-18 | |
| * | | | | | | | | | | | | | | Merge PR #781: Remove dead code [Universes.simplify_universe_context] | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #783: Remove some useless code in Term_typing | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge 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-17 | |
| | |_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | | Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body move... | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #879: Adding debug printers related to universes | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #874: Adding econstr printer to "include" file. | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #872: [travis] Display info on tested commit for PR builds. | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #865: RefMan-ext: fix some typos | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat... | Maxime Dénès | 2017-07-17 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | * \ \ \ \ \ \ \ \ \ \ | Merge PR #861: Fix typo in documentation for identity | Maxime Dénès | 2017-07-17 | |
| | | | | | | | | | | | | |\ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | | | | | | * | Fixing what was presumably a typo in the naming conventions file. | Hugo Herbelin | 2017-07-16 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | | | | | | | | | | | | | | | * | | Removing a dummy parameter in some FMapPositive statements. | Hugo Herbelin | 2017-07-16 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | ||||
| | | | | | | * | | | | | | | | | | | | | | | | Adapting to 91df40272 (body_of_constant_body moved to global). | Hugo Herbelin | 2017-07-16 | |
| | |_|_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | ||||
| | | * | | | | | | | | | | | | | | | | | | | Update with non structurally recursive |  william-lawvere | 2017-07-14 | |
| | | | | | * | | | | | | | | | | | | | | | | Adding debug printers related to universes in the default debugger source file. | Pierre-Marie Pédrot | 2017-07-14 | |
| | |_|_|_|/ / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | | | | | | | Fix a typo in dev/changes. | Pierre-Marie Pédrot | 2017-07-14 | |
| | | | | | * | | | | | | | | | | | | | | | Document the changes in API brought by this series of patches. | Pierre-Marie Pédrot | 2017-07-14 | |
| | | | | | * | | | | | | | | | | | | | | | Getting rid of abstraction breaking code in tclABSTRACT. | Pierre-Marie Pédrot | 2017-07-14 | |
| | | | | | | | | | | | | | | * | | | | | | [travis] Update testing to 4.05.0 + Camlp5 7.01 | Emilio Jesus Gallego Arias | 2017-07-13 | |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | | | | | | | | Removing a use of AUContext.instance in the STM. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Removing the uses of abstraction-breaking code in Lemmas. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | | | | | | * | | | | | | | | | Set version to 8.7+alpha. | Maxime Dénès | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Removing the uses of abstraction-breaking code in Obligations. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Remove the function Global.type_of_global_unsafe. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | The only abstraction-breaking function in Univ is now AUContext.instance. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Getting rid of AUContext abstraction breakers in Elimschemes. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Getting rid of AUContext abstraction breakers in Discharge. | Pierre-Marie Pédrot | 2017-07-13 | |
| | | | | | * | | | | | | | | | | | | | | Make the typeclass implementation fully compatible with universe polymorphism. | Pierre-Marie Pédrot | 2017-07-13 | |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |