| Commit message (Expand) | Author | Age |
* | Fix bugs 4389, 4390 and 4391 due to wrong handling of universe names | Matthieu Sozeau | 2015-10-27 |
* | Minor module cleanup : error HigherOrderInclude was never happening | Pierre Letouzey | 2015-10-25 |
* | Miscellaneous typos, spacing, US spelling in comments or variable names. | Hugo Herbelin | 2015-10-18 |
* | Lemmas accept the Local flag. | Pierre-Marie Pédrot | 2015-10-17 |
* | Remove -vm flag of coqtop. | Maxime Dénès | 2015-10-14 |
* | Fixing bug #4367: Wrong error message in unification. | Pierre-Marie Pédrot | 2015-10-14 |
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Fix Definition id := Eval <redexpr> in by passing the right universe | Matthieu Sozeau | 2015-10-12 |
* | Code cleaning in VM (with Benjamin). | Maxime Dénès | 2015-10-09 |
* | Fix Next Obligation to not raise an anomaly in case of mutual | Matthieu Sozeau | 2015-10-09 |
* | Axioms now support the universe binding syntax. | Pierre-Marie Pédrot | 2015-10-08 |
* | aux_file: export API to ease writing of a Proof Using annotator. | Enrico Tassi | 2015-10-08 |
* | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi | 2015-10-08 |
* | Spawn: use each socket exclusively for writing or reading | Enrico Tassi | 2015-10-08 |
* | Goptions: new value type: optional string | Enrico Tassi | 2015-10-08 |
* | Univs: fix FingerTree contrib. | Matthieu Sozeau | 2015-10-07 |
* | Univs: add Strict Universe Declaration option (on by default) | Matthieu Sozeau | 2015-10-07 |
* | Univs: fix handling of evar_map in identity coercion construction. | Matthieu Sozeau | 2015-10-05 |
* | Fix after rebase... | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix inference of the lowest sort for records. | Matthieu Sozeau | 2015-10-02 |
* | Univs: correcly compute the levels of records when they fall in Prop. | Matthieu Sozeau | 2015-10-02 |
* | Univs/program: handle side effects in obligations. | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix Show Universes. | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix environment handling in scheme building. | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix after rebase (from_ctx/from_env) | Matthieu Sozeau | 2015-10-02 |
* | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau | 2015-10-02 |
* | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau | 2015-10-02 |
* | Prevent States.intern_state and System.extern_intern from looking up files in... | Guillaume Melquiond | 2015-09-29 |
* | Remove some uses of Loadpath.get_paths. | Guillaume Melquiond | 2015-09-29 |
* | Make -load-vernac-object respect the loadpath. | Guillaume Melquiond | 2015-09-28 |
* | The -require option now accepts a logical path instead of a physical one. | Pierre-Marie Pédrot | 2015-09-25 |
* | Updating the documentation and the toolchain w.r.t. the change in -compile. | Pierre-Marie Pédrot | 2015-09-25 |
* | The -compile option now accepts ".v" files and outputs a warning otherwise. | Pierre-Marie Pédrot | 2015-09-25 |
* | Hopefully better names to constructors of internal_flag, as discussed | Hugo Herbelin | 2015-09-23 |
* | Give a way to control if the decidable-equality schemes are built like | Hugo Herbelin | 2015-09-23 |
* | Removing the generalization of the body of inductive schemes from | Hugo Herbelin | 2015-09-23 |
* | Fix #3948 Anomaly: unknown constant in Print Assumptions | Maxime Dénès | 2015-09-20 |
* | Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on. | Pierre-Marie Pédrot | 2015-09-15 |
* | Univs: Add universe binding lists to definitions | Matthieu Sozeau | 2015-09-14 |
* | Also there's an extra space in the error message. | mlasson | 2015-09-03 |
* | Code cleaning in Obligations. | Pierre-Marie Pédrot | 2015-08-22 |
* | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin | 2015-08-02 |
* | Give a way to control if the decidable-equality schemes are built like | Hugo Herbelin | 2015-08-02 |
* | Removing the generalization of the body of inductive schemes from | Hugo Herbelin | 2015-08-02 |
* | For convenience, making yes and on, and no and off synonymous in | Hugo Herbelin | 2015-08-02 |
* | Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874) | Guillaume Melquiond | 2015-07-28 |
* | Improving over 26aa224293 in reporting unexpected error during scheme creation. | Hugo Herbelin | 2015-07-27 |
* | Fixing bug #3736 (anomaly instead of error/warning/silence on | Hugo Herbelin | 2015-07-27 |
* | Option -type-in-type: added support in checker and making it contaminating | Hugo Herbelin | 2015-07-10 |
* | Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its | Hugo Herbelin | 2015-07-07 |