aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2019-04-23[ssr] under: Check that the number of hints and focused goals matchErik Martin-Dorel
2019-04-23[ssr] under(one-liner version): Do nf_betaiota in the last goalErik Martin-Dorel
As a result, the following: under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *) under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *) amounts to: under i: eq_bigr; [rewrite adnnC; over | cbv beta iota]. under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | cbv beta iota].
2019-04-23[ssr] under: Change the style of a few tests (over tactic vs. lemma)Erik Martin-Dorel
2019-04-23[ssr] under: Add a fancy test with several kinds of side-conditionsErik Martin-Dorel
2019-04-23[ssr] under: Move {beta_expand, unify_helper} in the module type (qualify them)Erik Martin-Dorel
2019-04-23[ssr] under: Strenghten over & Add test_big_andbErik Martin-Dorel
* Rely on a new tactic unify_helper that workarounds the fact [apply Under.under_done] cannot unify (?G i...) with (expr i...) in [|- @Under T (expr i...) (?G i...)] when expr is a constant expression, or has more than one var (i...). Idea: massage the expression with Ltac to obtain a beta redex. * Simplify test-suite/ssr/under.v by using TestSuite.ssr_mini_mathcomp and add a test-case [test_big_andb]. * Summary of commands to quickly test [under]: $ cd .../coq $ make plugins/ssr/ssreflect.vo plugins/ssr/ssrfun.vo plugins/ssr/ssrbool.vo $ cd test-suite $ touch prerequisite/ssr_mini_mathcomp.v $ make $ emacs under.v
2019-04-23[ssr] under: Extend the test-suite to exemplify most use casesErik Martin-Dorel
2019-04-23[ssr] under: generate missing Under subgoal for eq_bigl/eq_bigErik Martin-Dorel
in the particular case where the side-condition is phrased (_ : @eqfun bool I P1 P2) instead of (_ : forall x : I, P1 x = P2 x)
2019-04-23[ssr] under: Add support for one-liners "under (…) by [tac1|tac2]."Erik Martin-Dorel
Supported syntax: under i: eq_bigr by rewrite adnnC. (* ensure 1 Under subogal is created *) under i: eq_big by [rewrite adnnC | rewrite addnC]. (* 2 Under subgoals *) Equivalent, expanded form: under i: eq_bigr; [rewrite adnnC; over | idtac]. under i: eq_big; [rewrite adnnC; over | rewrite adnnC; over | idtac].
2019-04-23[ssr] over: also works on universally quantified goalsErik Martin-Dorel
2019-04-23[ide] update coq-ssreflect.lang wrt under tacticEnrico Tassi
2019-04-23[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"Erik Martin-Dorel
Both can be use to close the "under goals", in rewrite style or in closing-tactic style. Contrarily to the previous implementation that assumed "over : forall (T : Type) (x : T), @Under T x x <-> True" this new design won't require the Setoid library. Extend the test-suite (in test-suite/ssr/under.v)
2019-04-23[ssr] under: Rename bound variables a posteriori for cosmetic purposeEnrico Tassi
Rename the bound variables of the last (lambda) argument of the redex w.r.t. the varnames specified by the user. Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr>
2019-04-21Remove duplicate copy of _warn_if_duplicate_name.Jim Fehrle
2019-04-20Merge PR #9836: [schemes] Don't re-declare scheme side-effects that are ↵Enrico Tassi
already there. Reviewed-by: gares
2019-04-20Merge PR #9906: coq_makefile install target: error if any file is missingEnrico Tassi
Reviewed-by: gares
2019-04-20overlay for elpiEnrico Tassi
2019-04-20update elpi to version 1.2Enrico Tassi
2019-04-17Merge PR #9966: Add changes for -setEmilio Jesus Gallego Arias
2019-04-17Add changes for -setGaëtan Gilbert
I realized this was missing just as the PR got merged
2019-04-17Merge PR #9876: Command-line setters for optionsEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares
2019-04-17Merge PR #9891: [CI] Build CoqIDE for macOS on AzurePierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
2019-04-16Merge PR #9165: Recarg cleanupEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: herbelin Reviewed-by: mattam82 Ack-by: maximedenes
2019-04-16Merge PR #9898: Better error message when OCaml compiler not found for ↵Emilio Jesus Gallego Arias
native compute Reviewed-by: ejgallego
2019-04-16[doc] [kernel] Add docstrings for native interface functions.Emilio Jesus Gallego Arias
2019-04-16Better error message when OCaml compiler not found for native computeMaxime Dénès
Fixes #6699
2019-04-16[doc] Changes for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ast] [constrexpr] Make recursion_order_expr an AST node.Emilio Jesus Gallego Arias
This is a bit more uniform.
2019-04-16Update and fix documentation of Program Fixpoint with measureMaxime Dénès
2019-04-16Fix spurious argument of {measure}Maxime Dénès
Previsouly, it was silently ignored.
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
We make clearer which arguments are optional and which are mandatory. Some of these representations are tricky because of small differences between Program and Function, which share the same infrastructure. As a side-effect of this cleanup, Program Fixpoint can now be used with e.g. {measure (m + n) R}. Previously, parentheses were required around R.
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-26 23:14:44 +0000