| Age | Commit message (Collapse) | Author |
|---|
|
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>
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
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.
|
|
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
|
|
|
|
|
|
I had to reorganize the code a bit. The Context command moved to
comAssumption, as it is not so related to type classes. We were able to
remove a few hooks on the way.
|
|
One other call still remains, but will require to refactor some
section-handling code.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
|
|
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
|
|
Ack-by: JasonGross
Reviewed-by: ppedrot
|
|
RealField.v is slightly modified so that the ring/field tactics
consider the term (IZR (Z.pow_pos 10 _)) produced when parsing
exponents as constants.
|
|
Rather than integers '[0-9]+', numeral constant can now be parsed
according to the regexp '[0-9]+ ([.][0-9]+)? ([eE][+-]?[0-9]+)?'.
This can be used in one of the two following ways:
- using the function `Notation.register_rawnumeral_interpreter` in an OCaml plugin
- using `Numeral Notation` with the type `decimal` added to `Decimal.v`
See examples of each use case in the next two commits.
|
|
In anticipation of future uses of this token for non integer numerals.
|
|
|
|
#9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
|
|
- 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
|
|
Instead of just string (and empty strings for tokens without payload)
|
|
(warn if bar is a nonprimitive projection)
|
|
|
|
|
|
In that case the terminator and proof object have to be supplied in
the ?proof argument, or else we get an anomaly.
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
We add state handling to tactics.
TODO:
- [rewrite] `add_morphism_infer` creates problems as it opens a proof.
- [g_obligations] with_tac
|
|
Ack-by: gares
Ack-by: maximedenes
|
|
Previously, they were hard-wired in the ML code.
|
|
|
|
|
|
Eliminators can be:
- dependent: ... -> forall x (y : I x), P x y
- truncated: ... -> forall x (y : I x), P x
- funind like: ..-> forall x, P t
The user may provide a term t in `elim: t`
- t may be the last argument
- t may be the last "pattern" (standing for the last
argument of P)
We use unification to see if t (and its type) fits
in one of these cases (and/or to infer t).
This patch refuses to use unification in the HO case
eg `?T a = t` since the result is too often a false
positive.
|
|
This should make https://github.com/coq/coq/pull/9129 easier.
|
|
Reviewed-by: ejgallego
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82
|
|
Unknown impact so no tests.
|
|
Prevent errors when under annotating binders.
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
