Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Fast path in weak head reduction of applied atoms. | 2017-04-08 | |
* | Update the .mailmap file. | 2017-04-08 | |
* | Merge PR#461: [camlpX] Remove camlp4 compat layer. | 2017-04-07 | |
|\ | |||
* | | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac) | 2017-04-07 | |
* | | Merge PR#485: Document Show Match | 2017-04-07 | |
|\ \ | |||
* | | | Remove a forgotten rule for decl_mode from the Makefile. | 2017-04-07 | |
| | * | [travis] Overlay for PR#461: Camlp4 removal. | 2017-04-07 | |
| | * | [camlpX] Enrico's changes to camlp4 removal. | 2017-04-07 | |
| | * | [camlpX] Remove camlp4 compat layer. | 2017-04-07 | |
| |/ |/| | |||
* | | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ... | 2017-04-07 | |
|\ \ | |||
* \ \ | Merge PR#519: Faster side effects | 2017-04-07 | |
|\ \ \ | |||
| * | | | Inline the only use of hcons_j in Term_typing. | 2017-04-07 | |
* | | | | Merge PR#455: Farewell decl_mode | 2017-04-06 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#488: Adding a documentation for the new proof engine. | 2017-04-06 | |
|\ \ \ \ \ | |||
| * | | | | | Adding a documentation for the new proof engine. | 2017-04-06 | |
|/ / / / / | |||
| | * | | | Documenting the fact terms are only hashconsed outside of a section. | 2017-04-06 | |
* | | | | | Merge PR#508: Optimize pending evars | 2017-04-06 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#542: [travis] Add webhook to Gitter. | 2017-04-06 | |
|\ \ \ \ \ \ | |||
| * | | | | | | [travis] Add webhook to Gitter. | 2017-04-06 | |
| | | | | * | | [toplevel] Remove exception error printer in favor of feedback printer. | 2017-04-05 | |
| |_|_|_|/ / |/| | | | | | |||
* | | | | | | Merge PR#434: Optimizing array mapping in the kernel. | 2017-04-05 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#502: [pp] Add anomaly header to error messages. | 2017-04-04 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-04-03 | |
|\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR#533: Instances should obey universe binders even when defined by tac... | 2017-04-03 | |
| |\ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | Fix loading of ocamldebug printers. | 2017-04-03 | |
| | * | | | | | | | | Instances should obey universe binders even when defined by tactics. | 2017-04-03 | |
| |/ / / / / / / / | |||
* | | | | | | | | | Merge PR#417: No cast surgery in let in | 2017-04-03 | |
|\ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | Add test file for #4957. | 2017-04-03 | |
* | | | | | | | | | | Fix higher-order pattern variables not being printed as "@?" (bug #5431). | 2017-04-02 | |
* | | | | | | | | | | Fix documentation typo (bug #5433). | 2017-04-02 | |
* | | | | | | | | | | Simplify some proofs. | 2017-04-02 | |
* | | | | | | | | | | Declaring ltac plugin, so that static linking works. | 2017-04-01 | |
* | | | | | | | | | | Merge branch 'v8.6' into trunk | 2017-03-30 | |
|\ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / | |/| | | | | | | | | |||
| * | | | | | | | | | Merge PR#463: Run non-tactic comands without resilient_command | 2017-03-30 | |
| |\ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | 2017-03-30 | |
* | | | | | | | | | | | Merge PR#469: Added take to VectorDef | 2017-03-30 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | | Added take to VectorDef. | 2017-03-30 | |
* | | | | | | | | | | | | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | 2017-03-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / / / / / / | |/| | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | Merge PR#514: [travis] Backport from trunk: VST | 2017-03-29 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* | \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#506: [nit] Fix a couple incorrect uses of msg_error. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#521: Do so that "About" tells if a reference is a coercion. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#525: [ide] Fix typo in pp serialization. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | * | | | | | | | | Run non-tactic comands without resilient_command | 2017-03-29 | |
| | | | | |_|_|_|/ / / / / / / / | | | | |/| | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | | [ide] Fix typo in pp serialization. | 2017-03-29 | |
* | | | | | | | | | | | | | | | | Fixing missing PropFacts.v in Logic/vo.itarget. | 2017-03-28 | |
|/ / / / / / / / / / / / / / / | |||
| | | | | * / / / / / / / / / | [coqide] Protect against size_allocate race in proofview. | 2017-03-28 | |
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | Do so that "About" tells if a reference is a coercion. | 2017-03-27 | |
|/ / / / / / / / / / / / / | |||
| | | | | | | | | | | * | | More efficient check in validity of side-effects. | 2017-03-27 |