| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Merge PR #6769: Split closure cache and remove whd_both |  Maxime Dénès | 2018-03-09 |
| |\ | |||
| * \ | Merge PR #6923: Export options | Maxime Dénès | 2018-03-09 |
| |\ \ | |||
| * \ \ | Merge PR #6480: Allow Prop as source for coercions | Maxime Dénès | 2018-03-09 |
| |\ \ \ | |||
| * \ \ \ | Merge PR #6947: coqide: queries from the query window are routed there (fix #... | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #6818: Sphinx doc infrastructure | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ | |||
| | * | | | | | Moving Gitlab CI documentation build to the main Coq build. | Maxime Dénès | 2018-03-09 |
| | * | | | | | Integration of a sphinx-based documentation generator. | Maxime Dénès | 2018-03-09 |
| | * | | | | | Configure now fails with -with-doc yes when a doc dependency is missing. | Maxime Dénès | 2018-03-09 |
| * | | | | | | Merge PR #6895: [compat] Remove "Refolding Reduction" option. | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ | |||
| | | | | | | * | | Add an overlay for Equations and Ltac2. |  Pierre-Marie Pédrot | 2018-03-09 |
| | | | | | | * | | Documenting the Export modifier for options in CHANGES. | Pierre-Marie Pédrot | 2018-03-09 |
| | | | | | | * | | Implement the Export Set/Unset feature. | Pierre-Marie Pédrot | 2018-03-09 |
| | | | | | | * | | Export the various option localities in the API. | Pierre-Marie Pédrot | 2018-03-09 |
| | |_|_|_|_|/ / |/| | | | | | | |||
| | | | | | * | | doc and changes for coercion from prop/type |  charguer | 2018-03-09 |
| | | | | | * | | added test for coercion from type | charguer | 2018-03-09 |
| | | | | | * | | allow Prop as source for coercions | charguer | 2018-03-09 |
| | |_|_|_|/ / |/| | | | | | |||
| * | | | | | | Merge PR #6941: [toplevel] Respect COQ_COLORS environment variable | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6945: Fix error with univ binders on monomorphic records. | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6871: [build] Simpler byte/opt toplevel build. | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6155: Get rid of ' notation for Zpos in QArith | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / |/| | | | | | | | | |||
| * | | | | | | | | | Merge PR #6800: [checker] Printer cleanup. | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6747: Relax conversion of constructors according to the pCuIC model | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6328: Fix #6313: lost goals in nested ltac in refine | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6496: Generate typed generic code from ltac macros | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6937: Add empty compat file for Coq 8.8 | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry... | Maxime Dénès | 2018-03-09 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | * | | | | | | | | | | | More examples about shelve/given_up in tactic-in-terms. |  Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Cosmetic: add an expected newline in proof_global. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | A comment in Proofview.with_shelf. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Add an invariant on future goals in Proof.run_tactic. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Add an invariant on given up goals in class_tactics. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Proof engine: support for nesting tactic-in-term within other tactics. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Add function bind in option.ml. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Proof engine: using save_future_goal when relevant. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Proof engine: adding a function to save future goals including principal one. | Hugo Herbelin | 2018-03-08 |
| | | | | | * | | | | | | | | | | | Proof engine: consider the pair principal and future goals as an entity. | Hugo Herbelin | 2018-03-08 |
| | |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | | Merge PR #6522: Fix core hint database issue #6521 | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6928: gitlab: install num for all 4.06 jobs | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish... | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6893: Cleanup UState API usage | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | | | * | | | [compat] Remove "Refolding Reduction" option. |  Emilio Jesus Gallego Arias | 2018-03-08 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | * | | | | | | | | | | | Make most of TACTIC EXTEND macros runtime calls. | Maxime Dénès | 2018-03-08 |
| | |_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | | | | | Merge PR #6918: romega: get rid of EConstr.Unsafe | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | | | * | | coqide: queries from the query window are routed there (fix #5684) |  Enrico Tassi | 2018-03-08 |
| | | | | | | | | | | | | | | * | | | | | Fix error with univ binders on monomorphic records. |  Gaëtan Gilbert | 2018-03-08 |
| * | | | | | | | | | | | | | | | | | | | Merge PR #6817: [configure]: support for profiles | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |