| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-04-16 | Merge PR #7263: CHANGES: document COQFLAGS change | Enrico Tassi | |
| 2018-04-16 | CHANGES: document COQFLAGS change | Ralf Jung | |
| 2018-04-16 | Merge PR #7200: [ltac] Deprecate nameless fix/cofix. | Maxime Dénès | |
| 2018-04-16 | Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Maxime Dénès | |
| 2018-04-16 | Merge PR #7246: Add missing CHANGES entry for #6169. | Maxime Dénès | |
| 2018-04-15 | Update debugging.md | Jasper Hugunin | |
| This changed in https://github.com/coq/coq/commit/35961a4ff5a5b8c9b9786cbab0abd279263eb655 | |||
| 2018-04-15 | Merge PR #7247: Simplify CircleCI script | Gaëtan Gilbert | |
| 2018-04-15 | Merge PR #7252: Sphinx doc fix warnings | Théo Zimmermann | |
| 2018-04-15 | Simplify CircleCI script | Yishuai Li | |
| 2018-04-15 | [doc] [engine] Document `abort_on_undefined_evars`. | Emilio Jesus Gallego Arias | |
| 2018-04-14 | Merge PR #7250: Sphinx doc chapter 9 | Théo Zimmermann | |
| 2018-04-14 | [Sphinx] Build with warnings as errors | Maxime Dénès | |
| Most of these warnings should really be errors (ill-formed input, invalid cross references, etc.) so we make it the default. | |||
| 2018-04-14 | [Sphinx] Fix all remaining warnings. | Maxime Dénès | |
| 2018-04-14 | doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing | Clément Pit-Claudel | |
| The Ubuntu Font License requires substantially modified fonts to be renamed entirely. | |||
| 2018-04-14 | [sphinx] Fix many warnings. | Théo Zimmermann | |
| Including cross-reference TODOs. I took down the number of warnings from 300 to 50. | |||
| 2018-04-14 | [Sphinx] Add chapter 9. | Théo Zimmermann | |
| Chapter ported by Théo Zimmermann and Maxime Dénès. | |||
| 2018-04-14 | [Sphinx] Move chapter 9 to new infrastructure. | Théo Zimmermann | |
| 2018-04-14 | Merge PR #7136: Evar maps contain econstrs. | Pierre-Marie Pédrot | |
| 2018-04-14 | Merge PR #7217: Sphinx doc chapter 1 | Théo Zimmermann | |
| 2018-04-14 | Add missing CHANGES entry for #6169. | Théo Zimmermann | |
| Fixes #7243. | |||
| 2018-04-13 | Making tactic-in-term aware of "Set Ltac Debug". | Hugo Herbelin | |
| 2018-04-13 | Update the CI branch for Equations. | Théo Zimmermann | |
| 2018-04-13 | Overlay for econstr in Evd. | Gaëtan Gilbert | |
| 2018-04-13 | [coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233) | Enrico Tassi | |
| 2018-04-13 | univ minimization: comment [enforce_uppers] | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization [enforce_upper]: replace Option.get with match | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization: Partially let-lift [enforce_uppers] | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization: rename acc' -> enforce_uppers | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization: use shadowing more | Gaëtan Gilbert | |
| This avoids having multiple highly similar things in scope when we only want one of them. | |||
| 2018-04-13 | univ minimization: let-lift [not_lower] | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization: simplify try-with block around find_insts | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/ | Gaëtan Gilbert | |
| 2018-04-13 | univ minimization: simplify try-with block around [find u left] | Gaëtan Gilbert | |
| This makes it clear where the Not_found can come from. | |||
| 2018-04-13 | univ minimization: comment compare_constraint_type | Gaëtan Gilbert | |
| 2018-04-13 | niv minimization: remove [remove_lower] abbreviation | Gaëtan Gilbert | |
| It's not long, used only once and it's easier to understand what it does when it's inlined. | |||
| 2018-04-13 | minimize_univ_variables: bool*bool*univ*lowermap replaced by record | Gaëtan Gilbert | |
| 2018-04-13 | minimize_univ_variables: remove [and right] abbreviation. | Gaëtan Gilbert | |
| 2018-04-13 | universe normalisation: put equivalence class partition in UGraph | Gaëtan Gilbert | |
| ie don't go through having Eq constraints but directly to the unionfind. | |||
| 2018-04-13 | universe minimization: cleanup using standard combinators, open Univ | Gaëtan Gilbert | |
| eg Constraint.partition + filter instead of a complicated fold. | |||
| 2018-04-13 | Evar maps contain econstrs. | Gaëtan Gilbert | |
| We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. | |||
| 2018-04-13 | Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵ | Pierre-Marie Pédrot | |
| contains evars | |||
| 2018-04-13 | [ltac] Deprecate nameless fix/cofix. | Emilio Jesus Gallego Arias | |
| LTAC's `fix` and `cofix` do require access to the proof object inside the tactic monad when used without a name. This is a bit inconvenient as we aim to make the handling of the proof object purely functional. Alternatives have been discussed in #7196, and it seems that deprecating the nameless forms may have the best cost/benefit ratio, so opening this PR for discussion. See also #6171. | |||
| 2018-04-13 | [Sphinx] Add Chapter 1 | Maxime Dénès | |
| 2018-04-13 | [Sphinx] Move chapter 1 to new infrastructure | Maxime Dénès | |
| 2018-04-13 | Merge PR #7117: Sphinx doc chapter 29 | Théo Zimmermann | |
| 2018-04-13 | [ssr] fix delayed clears (fix #7045) | Enrico Tassi | |
| We take into account all future ipats, not just the ones in the current branch | |||
| 2018-04-13 | Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods. | Enrico Tassi | |
| 2018-04-12 | Merge PR #7222: [sphinx] Remove migration artefacts. | Maxime Dénès | |
| 2018-04-12 | Merge PR #7194: [warnings] Remove `set_current_loc` hack. | Maxime Dénès | |
| 2018-04-12 | Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by ↵ | Jason Gross | |
| removing the test. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |