aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-04-29Suppress warning message in stdlib.Guillaume Melquiond
2017-04-28Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."Maxime Dénès
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
2017-04-28Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."Maxime Dénès
I'm sure this was pushed by accident, since testing shows immediately that it breaks the compilation of the ssreflect plugin, hence all developments relying on it in Travis.
2017-04-28Using a more explicit algebraic type for evars of kind "MatchingVar".Hugo Herbelin
A priori considered to be a good programming style.
2017-04-28Renaming allow_patvar flag of intern_gen into pattern_mode.Hugo Herbelin
This highlights that this is a binary mode changing the interpretation of "?x" rather than additionally allowing patvar.
2017-04-28Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Maxime Dénès
let-ins
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-27Merge PR#583: [toplevel] More work on error handling.Maxime Dénès
2017-04-27Merge PR#586: trivial cleanup commits which does not change Coq APIMaxime Dénès
2017-04-27Merge PR#568: Remove tactic compatibility layerMaxime Dénès
2017-04-27Document the API changes.Pierre-Marie Pédrot
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-27Merge PR#585: Small typo in commentMaxime Dénès
2017-04-27Merge branch 'v8.6'Pierre-Marie Pédrot
2017-04-27contracting the type of "Pfedit.solve_by_implicit_tactic"Matej Košík
2017-04-26Small typo in commentVadim Zaliva
2017-04-25Give andb_prop a simpler proofJason Gross
No need to use `discriminate`. This is the hopefully uncontroversial part of https://github.com/coq/coq/pull/401.
2017-04-25[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
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.
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
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.
2017-04-25Fix an optimization failure in tclPROGRESS.Pierre-Marie Pédrot
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.
2017-04-25Merge PR#567: Fix bug #5377: @? patterns broken.Maxime Dénès
2017-04-25Merge PR#578: Fix nsatz not recognizing real literals.Maxime Dénès
2017-04-24[toplevel] Don't check proofs in -quick mode.Emilio Jesus Gallego Arias
This fixes a logical error introduced in ce2b2058587224ade9261cd4127ef4f6e94d356b Patch by @gares, closes https://coq.inria.fr/bugs/show_bug.cgi?id=5484
2017-04-24[toplevel] Don't mask critical exceptions in vernac interpretation.Emilio Jesus Gallego Arias
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
2017-04-24Adding a dedicated travis overlay for fiat-parsers.Pierre-Marie Pédrot
2017-04-24Removing various tactic compatibility layers in core tactics.Pierre-Marie Pédrot
2017-04-24Porting the firstorder plugin to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing compatibility layer in Leminv.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Command.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in congruence.Pierre-Marie Pédrot
2017-04-24Removing tactic compatibility layer in Micromega.Pierre-Marie Pédrot
2017-04-24Fix the API of the new pf_constr_of_global.Pierre-Marie Pédrot
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.
2017-04-24Removing trivial compatibility layer in refl_omega.Pierre-Marie Pédrot
2017-04-24Porting omega to the new tactic API.Pierre-Marie Pédrot
2017-04-24Removing trivial compatibility layer in omega.Pierre-Marie Pédrot
2017-04-24Porting generalize_dep to the new tactic engine.Pierre-Marie Pédrot
2017-04-24Removing the tclWEAK_PROGRESS tactical.Pierre-Marie Pédrot
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.
2017-04-24Removing the tclNOTSAMEGOAL primitive from the API.Pierre-Marie Pédrot
The only use in Equality is reimplemented in the new engine.
2017-04-24Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Maxime Dénès
2017-04-24Merge PR#574: Fix bug #5476: Ltac has an inconsistent view of hypotheses.Maxime Dénès
2017-04-24Merge PR#552: Miscelaneous commitsMaxime Dénès
2017-04-24Merge PR#577: Add bedrock targets src and facade to Travis CIMaxime Dénès
2017-04-24Merge PR#569: Documenting EConstr for developpers.Maxime Dénès
2017-04-24Merge PR#565: Remove VernacErrorMaxime Dénès
2017-04-24Merge PR#580: [ide] Fix #5482 "location for query commands" in IDE.Maxime Dénès
2017-04-24Merge PR#581: [toplevel] [emacs] Don't quote errors in emacs mode.Maxime Dénès
2017-04-24Merge PR#492: [travis] Pin camlp5 to the minimal version 6.14 for 4.02.3Maxime Dénès
2017-04-24Merge 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.3Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 15:50:41 +0000