| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
It was only required in the (not realistic) test case "test_over_2_2",
which happened to introduce evars after the context variables.
|
|
* "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
|
|
|
|
|
|
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].
|
|
|
|
|
|
|
|
* 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
|
|
|
|
in the particular case where the side-condition is phrased
(_ : @eqfun bool I P1 P2)
instead of
(_ : forall x : I, P1 x = P2 x)
|
|
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].
|
|
|
|
|
|
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)
|
|
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>
|
|
|
|
Still to do: renaming the bound variables afterwards
|
|
(Note: coq notations cannot contain \n)
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
|
|
|
|
|
|
* If this flag under=true: enable flag with_evars of refine_with
to create evar(s) if the "under lemma" has non-inferable args.
* Backward compatibility of ssr rewrite is kept.
* Fix test-suite/ssr/dependent_type_err.v
|
|
#9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
|
|
and to not use the VM
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Fixes #9844
|
|
|
|
|
|
Fixes #9840
|
|
It is important to fully normalize the term, *including inductive
parameters of constructors*; see https://github.com/coq/coq/issues/9840
for details on what goes wrong if this does not happen, e.g., from using
the vm rather than cbv.
Supersedes / closes #9655
|
|
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
Ack-by: proux01
|
|
- Improved reification for Micromega (support for #8764)
- Fixes #9268: Do not take universes into account in lia reification
Improve #9291 by threading the evar_map during reification.
Universes are unified.
- Remove (potentially cyclic) dependency over lra for Rle_abs
- Towards a complete simplex-based lia
fixes #9615
Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.
For scalability, nia is currently NOT performing this pre-processing.
- Lia is using the FSet library
manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
to work around a "leaked" hint breaking compatibility of eauto
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: jashug
|
|
|
|
Something like "("; [ s = SELF -> { s } ]; ")" in a GRAMMAR EXTEND in
a mlg file was causing an error message such as
OCAMLOPT f.ml
File "f.mlg", line 179, characters 55-67: # not in a semantic rule so line doesn't match anything in the mlg file
Error: This expression has type ('a, Extend.mayrec, 'a) Extend.symbol
but an expression was expected of type
('a, Extend.norec, 'b) Extend.symbol
Type Extend.mayrec is not compatible with type Extend.norec
It is now
COQPP f.mlg
Error: 'SELF' or 'NEXT' illegal in anonymous entry level
|
|
Instead of just string (and empty strings for tokens without payload)
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
warn if [bar] nonprimitive projection.
Reviewed-by: ppedrot
|
|
This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423.
This commit is no longer necessary
|
|
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8. We hereby assume that all file paths are valid UTF-8.
We also now actually test both python2 and python3 on the CI.
|
|
|
|
This should fix #9705
I'm kind-of cargo-cult coding here, from things like
https://docs.python.org/3/library/sys.html#sys.displayhook and
https://github.com/coq/coq/issues/9705#issuecomment-471996313, but
hopefully this fixes the issue without breaking anything. (I am really
a novice when it comes to the str/bytes distinction in python3.)
|
|
|
