| Age | Commit message (Collapse) | Author |
|---|
|
|
|
This file can be used to get in an environment ready to compile Coq
(with `nix-shell`) or to compile and install Coq (with `nix-build`).
|
|
PR #1120 was still buggy for the following reasons: variables in the
lhs of the notation were linked in the glob file while they have
nowhere to link to (the binder is the notation string) [I thought the
change I commited in links.html.out was actually improving but it was
an overlook, sorry.]
|
|
The two lines that this commit remove are spurious as a `git clean -dfx || true`
is already performed in `test-suite/coq-makefile/template/init.sh`.
While this resolves the accidental dependency on git, I am still unhappy with
this call of `git clean -dfx`.
|
|
|
|
alphabet).
|
|
|
|
We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.
We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).
|
|
Adding a file fixing #5996 and which uses this feature.
|
|
|
|
variables).
|
|
|
|
This concerns pr_value and message_of_value.
This has a few consequences. For instance, no more ad hoc message "a
term" or "a tactic", when not enough information is available for
printing, one gets a generic message "a value of type foobar".
But we also have more printers, satisfying e.g. request #5786.
|
|
We fix by interpreting the pattern in "change pat with term" in strict
mode by using the same interning code as for "match goal" (even if the
pattern is dropped afterwards).
|
|
This fixes also #5731, #6035, #5364.
|
|
|
|
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
|
|
|
|
|
|
|
|
clause of an inductive definitions
|
|
This should (hopefully) fix #5675.
|
|
Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
|
|
|
The test suite cases are preserved until the feature is actually removed.
|
|
|
|
Also add an output test for Suggest Proof Using.
This changes the .aux output: instead of getting a key
>context_used "$hyps;$suggest"
where $hyps is a list of the used hypotheses and $suggest is the
;-separated suggestions (or the empty string if Suggest Proof Using is
unset), there is a key
>context_used "$hyps"
and if Suggest Proof Using is set also a key
>suggest_proof_using "$suggest"
For instance instead of
112 116 context_used "B A;A B;All"
we get
112 116 context_used "B A"
112 116 suggest_proof_using "A B;All"
|
|
|
|
Morphism` forms.
|
|
printing-ony Notations
|
|
"_something")
|
|
inductive definition)
|
|
BZ#4852)
|
|
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
|
When a context variable x is of the form "x := body : Z",
romega is now made aware of this body. Technically, we reify an equation
x = body, and push a corresponding (eq_refl x) as argument of the
final do_omega.
See also the previous commit adding this same feature to omega
(fixing bug 142).
|
|
148)
For compatibility, this extra feature of omega could be disabled via
Unset Omega UseLocalDefs.
Caveat : for now, real let-ins inside goals or hyps aren't handled, use
some "cbv zeta" reduction if you want to get rid of them. And context
definitions whose types aren't Z or nat are ignored, some manual "unfold"
are still mandatory if expanding these definitions will help omega.
|
|
to escape non-UTF-8 file names)
|
|
|
|
BZ#5757)
|
|
cleared context.
|
|
BZ#4852)
This code simplification isn't that important, but it can trigger further
simplifications elsewhere, see for instance BZ#4852.
NB: normally, the extraction favors eta-expanded forms, since that's the usual
way to avoid issues about '_a type variables that cannot be generalized. But
the atomic eta-reductions done here shouldn't be problematic (no applications
put outside of functions).
|
|
|
|
|
|
This allows e.g. the following to work:
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).
We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.
Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.
|
|
|
|
|
|
|
|
|
|
|
|
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
