aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-04-27[refman] Fix typo.Théo Zimmermann
Noticed by Maxime Dénès.
2019-04-27[ci/gitlab] Remove after_switch message (not useful anymore).Théo Zimmermann
This was put in place for @coqbot to detect runner failures, but now the strategy is different.
2019-04-27Amending CYGWIN fix in 63e7fb56923 so that it does not add a warning on MacOS.Hugo Herbelin
Indeed, MacOS has a BSD uname and BSD uname does not support the -o option. Based on the following resources about uname compatility: https://stackoverflow.com/questions/3466166/how-to-check-if-running-in-cygwin-mac-or-linux https://en.wikipedia.org/wiki/Uname
2019-04-26Merge PR #9998: coq_makefile: do not pass -opt/-byte to coqc (fix #9974)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-26Merge PR #9981: [dune] Build coqc.byte executable.Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rgrinberg
2019-04-26Merge PR #9990: [opam] Use version to provide better package bounds.Théo Zimmermann
Reviewed-by: Zimmi48
2019-04-26Merge PR #10001: Add a typing colon in the output of the Search ssreflect ↵Enrico Tassi
vernacular Reviewed-by: gares
2019-04-26[opam] Use version to provide better package bounds.Emilio Jesus Gallego Arias
I copied this from Ralf Jung's submission to the Coq Package index, let's see if it works.
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
This has been a mess for quite a while, we try to improve it.
2019-04-25Merge PR #9999: Fix PKG in ide/.merlin.in for gtk3Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-25CoqIDE: install icons on macOSVincent Laporte
2019-04-25inferCumulativity: shortcut for all-Invariant inductivesGaëtan Gilbert
2019-04-25Add a typing colon in the output of the Search ssreflect vernacularErik Martin-Dorel
See also PR math-comp/math-comp#73
2019-04-25Fix PKG in ide/.merlin.in for gtk3Gaëtan Gilbert
2019-04-25CoqIDE: fix open-file dialog on macOSVincent Laporte
2019-04-25coq_makefile: do not pass -opt/-byte to coqc (fix #9974)Enrico Tassi
2019-04-25Merge Ltac2 pluginMaxime Dénès
2019-04-25Prepare merge into CoqMaxime Dénès
2019-04-24Merge PR #9988: [refman] Properly define token regexp.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24Merge PR #9989: [refman] Fix a quoting problem.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-04-24[refman] Fix a quoting problem.Théo Zimmermann
2019-04-24[refman] Properly define token regexp.Théo Zimmermann
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974
2019-04-24Fix proof bullet error helper (nosuchgoal)Gaëtan Gilbert
The [int] is incorrect for list focusing, we could work a bit harder to fix that. It's only used for pluralisation in the error message "no such goal(s)" so we could also ignore the issue.
2019-04-24[proof] Fix proof bullet error helper which was implemented as a hookEmilio Jesus Gallego Arias
We add the information on the proper layer by catching the low-level exception.
2019-04-24Allocate only one evar when applying a group of conversion tactics.Pierre-Marie Pédrot
2019-04-24Code factorization in conversion tactics.Pierre-Marie Pédrot
2019-04-24[dune] Build coqc.byte executable.Emilio Jesus Gallego Arias
This may be useful in a few cases, like testing compilation with byte-plugins; I chose to install it globally tho it is more of a developer target.
2019-04-23Deprecate the *_no_check variants of conversion tactics.Pierre-Marie Pédrot
2019-04-23Merge PR #9962: [native compiler] Encoding of constructors based on tagsPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-23[ssr] set under's tactic argument at LEVEL 3Erik Martin-Dorel
So if the underlying tactic "contains a ;" one should actually write: under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
2019-04-23[ssr] under: optimization of the tactic for (under eq_bigl => *)Erik Martin-Dorel
so it acts "more naturally" like (under eq_bigl; [hnf|]); move=> [*|]. Also: replace "by over." in the doc example with "over."
2019-04-23[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notationsErik Martin-Dorel
as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation.
2019-04-23[doc] ssr_under: a few improvementsEnrico Tassi
2019-04-23[ssr] under: Fix the defective form ("=> [*|*]" implied) and its docErik Martin-Dorel
* Add tests accordingly.
2019-04-23[ssr] Add small output test for "under eq_G => m do rewrite subnn"Erik Martin-Dorel
2019-04-23[ssr] under: Fix and extend the documentationErik Martin-Dorel
2019-04-23[ssr] under: Add iff support in side-conditionsErik Martin-Dorel
2019-04-23Merge PR #9889: Fix pretty-printing of primitive integersMaxime Dénès
Ack-by: JasonGross Ack-by: erikmd Reviewed-by: maximedenes Ack-by: proux01
2019-04-23Merge PR #9978: Remove duplicate copy of _warn_if_duplicate_name.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-23Merge PR #9973: update elpi to version 1.2Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-04-23[ssr] under: use varnames from the 1st ipat with multi-goal under lemmasErik Martin-Dorel
In particular, this enhances support for lemma eq_big (with 2 side-conditions).
2019-04-23[ssr] new syntax for the under tacticEnrico Tassi
2019-04-23[ssr] under: Simplify the over tacticErik Martin-Dorel
* Use ssr `by […|…]` and `apply:`
2019-04-23[ssr] under: Add doc for {under, over} & Add entry in CHANGES.mdErik Martin-Dorel
* For better uniformity, replace "intro-pattern" with "intro pattern" in the ssr doc.
2019-04-23[ssr] under: Add comment to justify the need for check_numgoalsErik Martin-Dorel
2019-04-23[ssr] over: Expose the new type of tactic for Ssrfwd.overtacErik Martin-Dorel
2019-04-23[ssr] Remove the unify_helper tactic that appears unnecessaryErik Martin-Dorel
It was only required in the (not realistic) test case "test_over_2_2", which happened to introduce evars after the context variables.
2019-04-23[ssr] under: Fix rewrite goals order when called from underErik Martin-Dorel
* "under"-specific behavior: the order of goals is kept even if one issues Global Set SsrOldRewriteGoalsOrder. * href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v
2019-04-23[ssr] over: Add Ssrfwd.overtac in the .mliErik Martin-Dorel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 03:12:04 +0000