| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Remove some unused values and types |  Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Rename Sos_lib.(||) -> parser_or to avoid (deprecated) Pervasives.or | Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum | Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Use [method!] to override methods (warning 7) | Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Fix omitted labels in function calls | Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Remove unused [rec] keywords | Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Locally disable some warnings. | Gaetan Gilbert | 2017-04-27 |
| | | |||
| * | Merge PR#583: [toplevel] More work on error handling. |  Maxime Dénès | 2017-04-27 |
| |\ | |||
| * \ | Merge PR#586: trivial cleanup commits which does not change Coq API | Maxime Dénès | 2017-04-27 |
| |\ \ | |||
| * \ \ | Merge PR#568: Remove tactic compatibility layer | Maxime Dénès | 2017-04-27 |
| |\ \ \ | |||
| | * | | | Document the API changes. |  Pierre-Marie Pédrot | 2017-04-27 |
| | | | | | |||
| * | | | | Merge PR#584: Give andb_prop a simpler proof | Maxime Dénès | 2017-04-27 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR#585: Small typo in comment | Maxime Dénès | 2017-04-27 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge branch 'v8.6' | Pierre-Marie Pédrot | 2017-04-27 |
| |\ \ \ \ \ \ | |||
| | | | | | * | | contracting the type of "Pfedit.solve_by_implicit_tactic" |  Matej Košík | 2017-04-27 |
| | |_|_|_|/ / |/| | | | | | |||
| | | * | | | | Small typo in comment |  Vadim Zaliva | 2017-04-26 |
| | |/ / / / |/| | | | | |||
| | | * | | | Give andb_prop a simpler proof |  Jason Gross | 2017-04-25 |
| | |/ / / |/| | | | | | | | No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401. | ||
| | | | * | [toplevel] Remove unused parameter from `Vernac.process_expr`. |  Emilio Jesus Gallego Arias | 2017-04-25 |
| | | | | | |||
| | | | * | [toplevel] Use exception information for error printing. | Emilio Jesus Gallego Arias | 2017-04-25 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a partial backtrack on 63cfc77ddf3586262d905dc351b58669d185a55e. In that commit, we disregarded exception and tried to print error messages just by listening to feedback. However, feedback error messages are not always emitted due to https://coq.inria.fr/bugs/show_bug.cgi?id=5479 Thus meanwhile it is safer to go back to printing the information present in exceptions until we tweak the STM. This fixes https://coq.inria.fr/bugs/show_bug.cgi?id=5467 and many other glitches not reported, such errors in nested proofs. | ||
| | * | | | Fix an optimization failure in tclPROGRESS. | Pierre-Marie Pédrot | 2017-04-25 |
| | | | | | | | | | | | | | | | | | | | | | | | | | Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails. | ||
| * | | | | Fix an optimization failure in tclPROGRESS. | Pierre-Marie Pédrot | 2017-04-25 |
| | | | | | | | | | | | | | | | | | | | | | | | | | Due to code reworking, a fastpath got anihilated because the slow path was computed altogether. We now only compute the slow check whenever the quick one fails. | ||
| | * | | | Merge PR#567: Fix bug #5377: @? patterns broken. | Maxime Dénès | 2017-04-25 |
| | |\ \ \ | |||
| * | \ \ \ | Merge PR#578: Fix nsatz not recognizing real literals. | Maxime Dénès | 2017-04-25 |
| |\ \ \ \ \ | |||
| | | | | | * | [toplevel] Don't check proofs in -quick mode. | Emilio Jesus Gallego Arias | 2017-04-24 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes a logical error introduced in ce2b2058587224ade9261cd4127ef4f6e94d356b Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484 | ||
| | | | | | * | [toplevel] Don't mask critical exceptions in vernac interpretation. | Emilio Jesus Gallego Arias | 2017-04-24 |
| | |_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Indeed we were not correctly backtracking in the case of StackOverflow. It makes sense to remove the inner handler which is a leftover of a previous attempt, and handle interpretation errors in load as non-recoverable. This fixes: https://coq.inria.fr/bugs/show_bug.cgi?id=5485 | ||
| | | | | * | Adding a dedicated travis overlay for fiat-parsers. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing various tactic compatibility layers in core tactics. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Porting the firstorder plugin to the new tactic API. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing compatibility layer in Leminv. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing tactic compatibility layer in Command. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing tactic compatibility layer in congruence. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing tactic compatibility layer in Micromega. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Fix the API of the new pf_constr_of_global. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead. | ||
| | | | | * | Removing trivial compatibility layer in refl_omega. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Porting omega to the new tactic API. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing trivial compatibility layer in omega. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Porting generalize_dep to the new tactic engine. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | |||
| | | | | * | Removing the tclWEAK_PROGRESS tactical. | Pierre-Marie Pédrot | 2017-04-24 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The only remaining use was applied on the unfold tactic, and the behaviours of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced by their argument tactic. | ||
| | | | | * | Removing the tclNOTSAMEGOAL primitive from the API. | Pierre-Marie Pédrot | 2017-04-24 |
| | |_|_|/ |/| | | | | | | | | | | | The only use in Equality is reimplemented in the new engine. | ||
| * | | | | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag. | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses. | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR#552: Miscelaneous commits | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ | |||
| | | | | | * \ | Merge PR#577: Add bedrock targets src and facade to Travis CI | Maxime Dénès | 2017-04-24 |
| | | | | | |\ \ | |||
| * | | | | | \ \ | Merge PR#569: Documenting EConstr for developpers. | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR#565: Remove VernacError | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE. | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode. | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3 | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#576: [ide] Rely less on `Stateid.dummy` | Maxime Dénès | 2017-04-24 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | * | | | | | | | | | | | | [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3 | Emilio Jesus Gallego Arias | 2017-04-24 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We now test: - 4.02.3 + 6.14 [and 32bits of those] - 4.04.0 + 6.17 this looks like what the official support set should be for 8.7, given that both Ubuntu and Debian will ship the first, then switch to the latter. We also pin xmlm to version 1.2.0 to workaround bug https://github.com/ocaml/opam-repository/issues/8815 | ||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |