| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-05-05 | [sphinx] Backport changes from #5979. | Théo Zimmermann | |
| 2018-05-05 | Two more uses of verbatim in doc. | Théo Zimmermann | |
| 2018-05-05 | Clean-up around cmd documentation. | Théo Zimmermann | |
| In particular, remove trailing dots. | |||
| 2018-05-05 | Remove duplicate Extraction commands documentation. | Théo Zimmermann | |
| 2018-05-05 | Add some refs in the Omega chapter. | Théo Zimmermann | |
| 2018-05-05 | More fixes in the Generalized Rewriting chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Replace remaining `@natural` by `@num`. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] More use of cmd references in Extraction chapter. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Use references for command Info. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] More reference fixes. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fix a porting mistake. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Use references for Print. | Théo Zimmermann | |
| 2018-05-05 | Fix error messages and make them consistent. | Théo Zimmermann | |
| All the error messages start with a capitalized letter and end with a dot. | |||
| 2018-05-05 | Add direct reference to congruence with. | Théo Zimmermann | |
| 2018-05-05 | Clean-up around options. | Théo Zimmermann | |
| - Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`. | |||
| 2018-05-05 | debug trivial and debug auto were not in the tactic index. | Théo Zimmermann | |
| 2018-05-05 | Fix failing example in refman. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fix some references. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Use option direct reference. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fix a typo that appeared during the migration. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Fix a hardcoded reference. | Théo Zimmermann | |
| 2018-05-05 | [sphinx] Backport reformulation. | Théo Zimmermann | |
| (cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2) | |||
| 2018-05-05 | [sphinx] Backport fix of typo. | Théo Zimmermann | |
| (cf. 6131f89f6b91c45e641dd877df8719fa77987453) | |||
| 2018-05-05 | Fix typo in Coercions chapter. | Théo Zimmermann | |
| 2018-05-04 | Merge PR #7416: Fix #7415. Printing Width was not applied to error messages. | Emilio Jesus Gallego Arias | |
| 2018-05-04 | Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`. | Pierre-Marie Pédrot | |
| 2018-05-03 | Merge PR #7134: When an error comes from loading the prelude, tell it ↵ | Emilio Jesus Gallego Arias | |
| happened at initialization time | |||
| 2018-05-03 | Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_subst | Pierre-Marie Pédrot | |
| 2018-05-03 | Fix #7415. Printing Width was not applied to error messages. | Pierre Courtieu | |
| 2018-05-03 | Merge PR #7304: Make `intro`/`intros` progress on existential variables. | Pierre-Marie Pédrot | |
| 2018-05-03 | Merge PR #7400: ci-vst.sh: use -o progs | Emilio Jesus Gallego Arias | |
| 2018-05-03 | Merge PR #7402: [ci]: add pidetop (fix #7336) | Emilio Jesus Gallego Arias | |
| 2018-05-02 | Making explicit that errors happen in one of five executation phases. | Hugo Herbelin | |
| The five phases are command line interpretation, initialization, prelude loading, rcfile loading, and sentence interpretation (only the two latters are located). We then parameterize the feedback handler with the given execution phase, so as to possibly annotate the message with information pertaining to the phase. | |||
| 2018-05-02 | Reporting when an error occurs at initialization time. | Hugo Herbelin | |
| Done by simplifying the three "try" liable to be caught at initialization time into one and by ensuring that the remaining one reports about being in initialization phase. | |||
| 2018-05-02 | Make "intro"/"intros" progress on existential variables. | Hugo Herbelin | |
| 2018-05-02 | [ci]: add pidetop (fix #7336) | Enrico Tassi | |
| 2018-05-02 | Merge PR #7339: [api] Move bullets and goals selectors to `proofs/` | Théo Zimmermann | |
| 2018-05-02 | Merge PR #7403: Makefile doc owners | Théo Zimmermann | |
| 2018-05-02 | Fix Makefile.ci pattern in CODEOWNERS | Maxime Dénès | |
| 2018-05-02 | Make doc owners also own Makefile.doc | Maxime Dénès | |
| 2018-05-02 | Merge PR #7394: [ci] [travis] Install num by default in all switches. | Gaëtan Gilbert | |
| 2018-05-02 | Merge PR #7370: Fix PHONY typo in coq_makefile | Enrico Tassi | |
| 2018-05-01 | Merge PR #7305: [toplevel] improve indentation | Emilio Jesus Gallego Arias | |
| 2018-05-01 | ci-vst.sh: use -o progs | Gaëtan Gilbert | |
| This is closer to what we mean than reproducing the default target without progs. | |||
| 2018-05-01 | Merge PR #7397: [ci] Fix #7396: VST is broken | Gaëtan Gilbert | |
| 2018-05-01 | [ci] Fix #7396: VST is broken | Emilio Jesus Gallego Arias | |
| This is due to our CI script relying on their makefile internals, unfortunately we still have to do this to avoid timeouts. | |||
| 2018-05-01 | [api] Move bullets and goals selectors to `proofs/` | Emilio Jesus Gallego Arias | |
| `Vernacexpr` lives conceptually higher than `proof`, however, datatypes for bullets and goal selectors are in `Vernacexpr`. In particular, we move: - `proof_bullet`: to `Proof_bullet` - `goal_selector`: to a new file `Goal_select` | |||
| 2018-04-30 | [ci] [travis] Install num by default in all switches. | Emilio Jesus Gallego Arias | |
| This makes sense and simplifies the script a bit. In preparation for a more uniform, Docker-based base image. | |||
| 2018-04-30 | Merge PR #7379: [doc] Update Sphinx build instructions for Debian derivatives. | Théo Zimmermann | |
| 2018-04-30 | Merge PR #6935: Separate universe minimization and evar normalization functions | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |