aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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.
2019-04-16Command-line setters for optionsGaëtan Gilbert
TODO coqproject handling (for now it can be done through -arg I guess)
2019-04-16[CI/Azure/macOS] Set MACOSX_DEPLOYMENT_TARGET to 10.12Vincent Laporte
2019-04-16[CI/Azure/macOS] Install Coq into an artifactVincent Laporte
2019-04-15Update critical-bugsPierre Roux
2019-04-15[vm] Protect accu and coq_envPierre Roux
Protect accu and coq_env against GC calls in the VM when calling primitive integer functions on 32 bits architecture.
2019-04-15[native compiler] Encoding of constructors based on tagsMaxime Dénès
This serves two purposes: 1. It makes the native compiler use the same encoding and lambda-representation as the bytecode compiler 2. It avoid relying on fragile invariants relating tags and constructor indices. For example, previously, the mapping from indices to tags had to be increasing.
2019-04-15[native compiler] Remove unused universe argument in LmakeblockMaxime Dénès
2019-04-15[native compiler] Distinguish constant constructors in lambda codeMaxime Dénès
2019-04-15[CI/Azure/macOS] Build CoqIDEVincent Laporte
2019-04-15[CoqIDE] Fix build system for macOSVincent Laporte
2019-04-15[CI] Print test-suite log on failure (macOS/Azure)Vincent Laporte
2019-04-15Merge PR #9927: Don't store closures in summary (reduction effects)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-04-15Merge PR #9959: [native compiler] Remove `Lconstruct` from lambda code.Pierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2019-04-14[native compiler] Remove now unused GconstructMaxime Dénès
2019-04-14[native compiler] Remove `Lconstruct` from lambda code.Maxime Dénès
This is a step towards unifying the higher level ILs of the native and bytecode compilers. See https://github.com/coq/coq/projects/17
2019-04-14Merge PR #9957: Add missing build dependency in `coq.opam`Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-14Fix coq/coq#9956Erik Martin-Dorel
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-20 07:50:35 +0000