| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Add some missing flushes in configure. |  Maxime Dénès | 2018-03-06 |
| * | Merge PR #6917: Fix failing packaging job. | Maxime Dénès | 2018-03-06 |
| |\ | |||
| * \ | Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ... | Maxime Dénès | 2018-03-06 |
| |\ \ | |||
| * \ \ | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file. | Maxime Dénès | 2018-03-06 |
| |\ \ \ | |||
| * \ \ \ | Merge PR #6896: [compat] Remove NOOP deprecated options. | Maxime Dénès | 2018-03-06 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #6824: Remove deprecated options related to typeclasses. | Maxime Dénès | 2018-03-06 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #6900: [compat] Remove "Tactic Pattern Unification" | Maxime Dénès | 2018-03-06 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | Maxime Dénès | 2018-03-06 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6901: [compat] Remove "Injection L2R Pattern Order" | Maxime Dénès | 2018-03-06 |
| |\ \ \ \ \ \ \ \ | |||
| | | | | | | | | * | Fix failing packaging job. |  Théo Zimmermann | 2018-03-05 |
| | |_|_|_|_|_|_|/ |/| | | | | | | | |||
| | | | | | | * | | [ssreflect] Export parsing witnesses in mli file. |  Emilio Jesus Gallego Arias | 2018-03-05 |
| | |_|_|_|_|/ / |/| | | | | | | |||
| * | | | | | | | Merge PR #6855: Update headers following #6543. | Maxime Dénès | 2018-03-05 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad | Maxime Dénès | 2018-03-05 |
| |\ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | [compat] Remove NOOP and alias deprecated options. | Emilio Jesus Gallego Arias | 2018-03-04 |
| | | | | | | * | | | Remove deprecated options related to typeclasses. | Théo Zimmermann | 2018-03-04 |
| | | | | | | |/ / | |||
| * | | | | | | | | Merge PR #935: Handling evars in the VM | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / |/| | | | | | | | |||
| | | * | | | | | | ssr: ipats: V82.tactic ~nf_evars:false everywhere |  Enrico Tassi | 2018-03-04 |
| | | * | | | | | | Proofview: V82.tactic option to not normalize evars | Enrico Tassi | 2018-03-04 |
| | | * | | | | | | ssr: rewrite Ssripats and Ssrview in the tactic monad | Enrico Tassi | 2018-03-04 |
| | | * | | | | | | tactics: export e_reduct_in_concl | Enrico Tassi | 2018-03-04 |
| | | * | | | | | | reductionops: remove dead code "bind_assum" | Enrico Tassi | 2018-03-04 |
| | | * | | | | | | proofview: debug API to print a goal | Enrico Tassi | 2018-03-04 |
| * | | | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5. | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6736: [toplevel] Move beautify to its own pass. | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / |/| | | | | | | | | |||
| * | | | | | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret... | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay... | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872] | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6882: Harden gitattributes against core.whitespace configuration. | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ... | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6676: [proofview] goals come with a state | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #915: Fix rewrite in * side conditions | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document sup... | Maxime Dénès | 2018-03-04 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | * | | | | | | Removing test for bug #2850. |  Pierre-Marie Pédrot | 2018-03-03 |
| | | | | | | | | | | | | | * | | | | | | Adding a test file for evar handling in the VM. | Pierre-Marie Pédrot | 2018-03-03 |
| | | | | | | | | | | | | | * | | | | | | Handling evars in the VM. | Pierre-Marie Pédrot | 2018-03-03 |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | * | | [compat] Remove "Tactic Pattern Unification" | Emilio Jesus Gallego Arias | 2018-03-03 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | * | | [compat] Remove "Intuition Iff Unfolding" | Emilio Jesus Gallego Arias | 2018-03-03 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | * | | [compat] Remove "Injection L2R Pattern Order" | Emilio Jesus Gallego Arias | 2018-03-03 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | * | | | CHANGES entry for #6791. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | * | | | Remove 8.5 compatibility support. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | * | | | Remove VOld compatibility flag. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | * | | | Turn warning for deprecated notations on. | Théo Zimmermann | 2018-03-02 |
| | | | | | | | | | | | | * | | | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann | 2018-03-02 |
| | |_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | |||
| | | | | | | | | | * | | | | | [VM] Unify Const_sorts and Const_type, and remove Vsort. | Maxime Dénès | 2018-03-02 |
| | |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | |||
| | | | | | | | * | | | | | | [stm] Partial fix for bug #6884 [location missing from replay nodes] | Emilio Jesus Gallego Arias | 2018-03-02 |
| | | | | | * | | | | | | | | Harden gitattributes against core.whitespace configuration. |  Gaëtan Gilbert | 2018-03-01 |
| | |_|_|_|/ / / / / / / / |/| | | | | | | | | | | | |||
| | | | | * | | | | | | | | Fix #6878: univ undefined for [with Definition] bad instance size. | Gaëtan Gilbert | 2018-03-01 |
| | |_|_|/ / / / / / / / |/| | | | | | | | | | | |||
| | | * | | | | | | | | | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". |  Hugo Herbelin | 2018-03-01 |
| | | | |_|/ / / / / / | | |/| | | | | | | | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |