| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | [camlpX] Remove camlp4 compat layer. |  Emilio Jesus Gallego Arias | 2017-04-07 |
| * | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ... |  Maxime Dénès | 2017-04-07 |
| |\ | |||
| * \ | Merge PR#519: Faster side effects | Maxime Dénès | 2017-04-07 |
| |\ \ | |||
| | * | | Inline the only use of hcons_j in Term_typing. |  Pierre-Marie Pédrot | 2017-04-07 |
| * | | | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 |
| |\ \ \ | |||
| * \ \ \ | Merge PR#488: Adding a documentation for the new proof engine. | Maxime Dénès | 2017-04-06 |
| |\ \ \ \ | |||
| | * | | | | Adding a documentation for the new proof engine. | Pierre-Marie Pédrot | 2017-04-06 |
| |/ / / / | |||
| | | * | | Documenting the fact terms are only hashconsed outside of a section. | Pierre-Marie Pédrot | 2017-04-06 |
| * | | | | Merge PR#508: Optimize pending evars | Maxime Dénès | 2017-04-06 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR#542: [travis] Add webhook to Gitter. | Maxime Dénès | 2017-04-06 |
| |\ \ \ \ \ | |||
| | * | | | | | [travis] Add webhook to Gitter. |  Théo Zimmermann | 2017-04-06 |
| | | | | | * | [toplevel] Remove exception error printer in favor of feedback printer. | Emilio Jesus Gallego Arias | 2017-04-05 |
| | |_|_|_|/ |/| | | | | |||
| * | | | | | Merge PR#434: Optimizing array mapping in the kernel. | Maxime Dénès | 2017-04-05 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR#502: [pp] Add anomaly header to error messages. | Maxime Dénès | 2017-04-04 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-04-03 |
| |\ \ \ \ \ \ \ | |||
| | * \ \ \ \ \ \ | Merge PR#533: Instances should obey universe binders even when defined by tac... | Maxime Dénès | 2017-04-03 |
| | |\ \ \ \ \ \ \ | |||
| * | | | | | | | | | Fix loading of ocamldebug printers. | Pierre-Marie Pédrot | 2017-04-03 |
| | | * | | | | | | | Instances should obey universe binders even when defined by tactics. |  Gaetan Gilbert | 2017-04-03 |
| | |/ / / / / / / | |||
| * | | | | | | | | Merge PR#417: No cast surgery in let in | Maxime Dénès | 2017-04-03 |
| |\ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | Add test file for #4957. | Maxime Dénès | 2017-04-03 |
| * | | | | | | | | | Fix higher-order pattern variables not being printed as "@?" (bug #5431). |  Guillaume Melquiond | 2017-04-02 |
| * | | | | | | | | | Fix documentation typo (bug #5433). | Guillaume Melquiond | 2017-04-02 |
| * | | | | | | | | | Simplify some proofs. | Guillaume Melquiond | 2017-04-02 |
| * | | | | | | | | | Declaring ltac plugin, so that static linking works. |  Hugo Herbelin | 2017-04-01 |
| * | | | | | | | | | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-30 |
| |\ \ \ \ \ \ \ \ \ | | |/ / / / / / / | |/| | | | | | | | |||
| | * | | | | | | | | Merge PR#463: Run non-tactic comands without resilient_command | Maxime Dénès | 2017-03-30 |
| | |\ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond | 2017-03-30 |
| * | | | | | | | | | | Merge PR#469: Added take to VectorDef | Maxime Dénès | 2017-03-30 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | | | Added take to VectorDef. |  George Stelle | 2017-03-30 |
| * | | | | | | | | | | | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | Maxime Dénès | 2017-03-30 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | Maxime Dénès | 2017-03-29 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-29 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / / / / / | |/| | | | | | | | | | | | |||
| | * | | | | | | | | | | | | Merge PR#514: [travis] Backport from trunk: VST | Maxime Dénès | 2017-03-29 |
| | |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * | \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#506: [nit] Fix a couple incorrect uses of msg_error. | Maxime Dénès | 2017-03-29 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#521: Do so that "About" tells if a reference is a coercion. | Maxime Dénès | 2017-03-29 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#525: [ide] Fix typo in pp serialization. | Maxime Dénès | 2017-03-29 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | * | | | | | | | Run non-tactic comands without resilient_command |  Tej Chajed | 2017-03-29 |
| | | | | | |_|_|_|/ / / / / / / | | | | |/| | | | | | | | | | | |||
| | * | | | | | | | | | | | | | | [ide] Fix typo in pp serialization. | Emilio Jesus Gallego Arias | 2017-03-29 |
| * | | | | | | | | | | | | | | | Fixing missing PropFacts.v in Logic/vo.itarget. | Hugo Herbelin | 2017-03-28 |
| |/ / / / / / / / / / / / / / | |||
| | | | | | * / / / / / / / / | [coqide] Protect against size_allocate race in proofview. | Emilio Jesus Gallego Arias | 2017-03-28 |
| | |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | |||
| | * | | | | | | | | | | | | Do so that "About" tells if a reference is a coercion. | Hugo Herbelin | 2017-03-27 |
| |/ / / / / / / / / / / / | |||
| | | | | | | | | | | | * | More efficient check in validity of side-effects. | Pierre-Marie Pédrot | 2017-03-27 |
| | | | | | | | | | | | * | Adding the size of the opaquetab in its representation. | Pierre-Marie Pédrot | 2017-03-27 |
| | | | | | | | | | | | * | Fix hashconsing of terms in the kernel. | Pierre-Marie Pédrot | 2017-03-27 |
| | |_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | |||
| | | | * | | | | | | | | [travis] Backport from trunk: VST | Emilio Jesus Gallego Arias | 2017-03-24 |
| | | |/ / / / / / / / | |||
| * | | | | | | | | | | Merge PR#489: [travis] Add VST | Maxime Dénès | 2017-03-24 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| | | | | * | | | | | | | [stm] Remove some obsolete vernacs/classification. | Emilio Jesus Gallego Arias | 2017-03-24 |
| | | * | | | | | | | | | [nit] Fix a couple incorrect uses of msg_error. | Emilio Jesus Gallego Arias | 2017-03-24 |
| | | | |/ / / / / / / | | |/| | | | | | | | |||
| | * / | | | | | | | | [travis] Add VST | Emilio Jesus Gallego Arias | 2017-03-24 |
| | |/ / / / / / / / | |||
| | | | | * | | | | | Applying same convention as in Definition for printing type in a let in. | Hugo Herbelin | 2017-03-24 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |