| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-06-22 | Merge PR#817: [stm] Fix route setting on VtQuery | Maxime Dénès | |
| 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 | 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 | |
| 2017-06-16 | Move (part of) tests from checker to success | Amin Timany | |
| Due to some unknown problem coqchk fails on some inductive types when it is compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis tests. | |||
| 2017-06-16 | Remove Warnings: unused value ... | Amin Timany | |
| 2017-06-16 | Checker add test for non-trivial constraints | Amin Timany | |
| 2017-06-16 | Properly instantiate contexts before pushing | Amin Timany | |
| 2017-06-16 | Enable the checking of ind subtyping in checker | Amin Timany | |
| 2017-06-16 | Document cumulativity for inductive types | Amin Timany | |
| 2017-06-16 | Change the option to Set Inductive Cumulativity | Amin Timany | |
| This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier. | |||
| 2017-06-16 | Add printing of cumulativity in inductive types | Amin Timany | |
| 2017-06-16 | Move univops from kernel to library | Amin Timany | |
| 2017-06-16 | Correct coqchk checking subtyping relation for inductives | Amin Timany | |
| 2017-06-16 | Correct coqchk reduction | Amin Timany | |
| 2017-06-16 | Simplify Univ.ml | Amin Timany | |
| 2017-06-16 | Fix a bug | Amin Timany | |
| Incorrect environment was used when checking subtyping information of inductive types. | |||
| 2017-06-16 | Disable debug printing | Amin Timany | |
| Fix a mistake in record declaration | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |