| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-25 | Exporting general-purpose functions on goal contexts from "logic.ml" to ↵ | Hugo Herbelin | |
| "tactics.ml". This is in preparation of move of "assert" from old to new proof engine. | |||
| 2017-06-25 | Adding intermediate entry point to create an evar in empty rel_context. | Hugo Herbelin | |
| 2017-06-23 | Merge PR#824: Fix printers | Maxime Dénès | |
| 2017-06-23 | Merge PR#821: [vernac] Remove stale bool parameter from ↵ | Maxime Dénès | |
| `VernacStartTheoremProof` | |||
| 2017-06-23 | Merge PR#820: [ide] Correct more merging errors. | Maxime Dénès | |
| 2017-06-23 | Merge PR#815: STM: par: report no error to UIs in non-solve mode | Maxime Dénès | |
| 2017-06-23 | Merge PR#794: Cleanup of ltac cmxs | Maxime Dénès | |
| 2017-06-23 | Merge PR#762: [vernac] Fix unneeded mutual references in Obligations | Maxime Dénès | |
| 2017-06-22 | Merge PR#817: [stm] Fix route setting on VtQuery | Maxime Dénès | |
| 2017-06-22 | Add missing definition and fix #use include;; as suggested by @amintimany. | Théo Zimmermann | |
| 2017-06-21 | [vernac] Remove stale bool parameter from `VernacStartTheoremProof` | Emilio Jesus Gallego Arias | |
| `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. | |||
| 2017-06-21 | [ide] Correct more merging errors. | Emilio Jesus Gallego Arias | |
| This file doesn't want to leave us. | |||
| 2017-06-20 | [stm] Fix route setting on VtQuery | Emilio Jesus Gallego Arias | |
| This is a fix for a mistake in d8874dd855d748aaaf504890487ab15ffd7a677d , where we forgot to propagate the route parameter. | |||
| 2017-06-20 | STM: par: report no error to UIs in non-solve mode | Enrico Tassi | |
| Used to report to the UI an Error feedback message whenever a worker was non making any progress. This is wrong since no-progress is fine (as long as one does not specify "solve") | |||
| 2017-06-20 | [vernac] Remove forward hooks from Obligations. | Emilio Jesus Gallego Arias | |
| This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references. | |||
| 2017-06-20 | [vernac] Remove unused hooks. | Emilio Jesus Gallego Arias | |
| These hooks are not used (leftovers?) and IMHO they should not be. | |||
| 2017-06-20 | Merge PR#742: Fix `make TIMED=1` garbage | Maxime Dénès | |
| 2017-06-20 | Merge PR#774: [ide] Add route_id parameter to query call. | Maxime Dénès | |
| 2017-06-20 | Merge PR#793: Fixing restriction of existential variables regarding evar_store | Maxime Dénès | |
| 2017-06-20 | Merge PR#807: romega: fix a slowdown | Maxime Dénès | |
| 2017-06-20 | Merge PR#803: Clean ssr | Maxime Dénès | |
| 2017-06-20 | Merge PR#790: Direct link to Travis branch builds. | Maxime Dénès | |
| 2017-06-20 | Merge PR#779: Each user overlay goes into its own file. | Maxime Dénès | |
| 2017-06-19 | Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topological | Maxime Dénès | |
| 2017-06-19 | Merge PR#777: Improving documentation of tactic "move" (report #4561) | Maxime Dénès | |
| 2017-06-19 | Merge PR#760: Fixing base_include after loc is an option + a better test ↵ | Maxime Dénès | |
| that #use"include" works | |||
| 2017-06-19 | Merge PR#795: [ide] Better exn printing. [fixes BZ#5524] | Maxime Dénès | |
| 2017-06-19 | Merge PR#613: Cumulativity for inductive types | Maxime Dénès | |
| 2017-06-19 | Test case for bug 5578. | Maxime Dénès | |
| 2017-06-19 | Merge PR#727: [tactics] Fix summary registration of global hint variable. | Maxime Dénès | |
| 2017-06-19 | Fix typo in comment. | Maxime Dénès | |
| 2017-06-19 | Merge PR#784: API additions for coq-dpdgraph | Maxime Dénès | |
| 2017-06-19 | Merge PR#755: "There are pending proofs" error message now lists the name of ↵ | Maxime Dénès | |
| the proofs. | |||
| 2017-06-18 | [ide] Add route_id parameter to query call. | Emilio Jesus Gallego Arias | |
| This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. | |||
| 2017-06-18 | [ide] Better exn printing. [fixes BZ#5524] | Emilio Jesus Gallego Arias | |
| Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies. | |||
| 2017-06-16 | Merge PR#804: Increase the time limit on 4366.v to make gitlab work better. | Maxime Dénès | |
| 2017-06-16 | romega: avoid potential slowdown when changing concl by reified version | Pierre Letouzey | |
| On some benchmarks provided by Chantal Keller a long time ago, romega was abnormally slow compared to omega (or lia). It turned out that the change of concl by reified version was triggering unnecessary unfolds of Z.add, instead of unfolding ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by the various Parameter Inline : no more indirections, Z_as_Int.plus is directly Z.add. Also use Tactics.convert_concl_no_check for this "change", as recommended by PMP. | |||
| 2017-06-16 | Merge PR#759: don't leak unqualified identifiers from the macro | Maxime Dénès | |
| 2017-06-16 | Add coq-dpdgraph to gitlab CI | Gaëtan Gilbert | |
| 2017-06-16 | "There are pending proofs" error message now lists the name of the proofs. | Théo Zimmermann | |
| This closes https://coq.inria.fr/bugs/show_bug.cgi?id=5275 | |||
| 2017-06-16 | Increase the time limit on 4366.v to make gitlab work better. | Gaëtan Gilbert | |
| 2017-06-16 | Each user overlay goes into its own file. | Théo Zimmermann | |
| This will avoid stupid merge conflicts in the future. | |||
| 2017-06-16 | Removing Proof_type from the API. | Pierre-Marie Pédrot | |
| Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead. | |||
| 2017-06-16 | Remove the last use of the low-level Proof_type API in ssr. | Pierre-Marie Pédrot | |
| 2017-06-16 | Fix a bug in cumulativity | Amin Timany | |
| 2017-06-16 | A short cleanup | Amin Timany | |
| 2017-06-16 | use map_constr more efficiently | Amin Timany | |
| 2017-06-16 | Optimization | Amin Timany | |
| Only try using cumulativity in conversion/subtyping if the universe instances are non-empty | |||
| 2017-06-16 | Use a smart map_constr | Amin Timany | |
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |