| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. | Emilio Jesus Gallego Arias | |
| In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. | |||
| 2018-05-04 | Merge PR #7416: Fix #7415. Printing Width was not applied to error messages. | Emilio Jesus Gallego Arias | |
| 2018-05-04 | Merge branch 'master' of https://github.com/ybertot/plugin_tutorials | Yves Bertot | |
| 2018-05-04 | adds an explanation to Cmd8 | Yves Bertot | |
| 2018-05-04 | remove a typo | Yves Bertot | |
| 2018-05-04 | remove errors in the documentation | Yves Bertot | |
| 2018-05-04 | remove errors in the documentation | Yves Bertot | |
| 2018-05-04 | adds a comment in simple_print.ml and a plugin declaration in g_tuto1.ml4 | Yves Bertot | |
| 2018-05-04 | .gitignore fine-tuning | Yves Bertot | |
| 2018-05-04 | Now a command to access the value of a constant | Yves Bertot | |
| 2018-05-04 | adds more packaging boilerplate in tuto0 | Yves Bertot | |
| 2018-05-04 | finished type-checking examples | Yves Bertot | |
| 2018-05-04 | Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`. | Pierre-Marie Pédrot | |
| 2018-05-04 | Fix #7413: coqdep warning on repeated files | Gaëtan Gilbert | |
| The same warning exists in ocamllibdep so I copied the change there. Detecting when 2 paths are the same is approximate, eg ././a.ml and a.ml are considered different. Implementing realpath probably isn't worth doing for this warning. | |||
| 2018-05-04 | follows G. Gilbert's suggestion to have polymorphism following a flag | Yves Bertot | |
| 2018-05-04 | A modified version that includes code proposed by G. Gilbert | Yves Bertot | |
| 2018-05-04 | This revision contains a simple Check command. | Yves Bertot | |
| 2018-05-03 | little cleanup on the defining command, and question in comments | Yves Bertot | |
| 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 | This version contains a simple command that defines a new constant | Yves Bertot | |
| 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 | Add .byte targets for every bestocaml target | Gaëtan Gilbert | |
| This makes it easier to compile our executables for debug purposes. | |||
| 2018-05-03 | Merge PR #7304: Make `intro`/`intros` progress on existential variables. | Pierre-Marie Pédrot | |
| 2018-05-03 | Fixes issue #7083 / Windows build: Unify build logging to console (for ↵ | Michael Soegtrop | |
| appveyor) and files | |||
| 2018-05-03 | Fixes issue #7081 / Windows build: strip in lablgtk build can fail randomly | Michael Soegtrop | |
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |