| Age | Commit message (Collapse) | Author |
|---|
|
Updated doc, but not tests-suite yet.
|
|
Error messages were outdated.
|
|
|
|
|
|
|
|
|
|
Documentation also updated.
|
|
Putting utf8 everywhere helps the maintainance of the online refman.
And anyway, this is the way to go. We should also chase and migrate
the few remaining iso-latin-1 files elsewhere in the sources.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
reference" and "simpl pattern" in the code (maybe we should have
merged them instead, but I finally decided to enforce their
difference, even if some compatibility is to be preversed - the idea
is that at some time "simpl reference" would only call a weak-head
simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n)
rather than S(S(n)) which could be useful for better using induction
hypotheses.
In the process we also implement the following:
- 'simpl "+"' is accepted to reduce all applicative subterms whose
head symbol is written "+" (in the toplevel scope); idem for
vm_compute and native_compute
- 'simpl reference' works even if reference has maximally inserted
implicit arguments (this solves the "simpl fst" incompatibility)
- compatibility of ltac expressions referring to vm_compute and
native_compute with functor application should now work (i.e.
vm_compute and native_compute are now taken into account in
tacsubst.ml)
- for compatibility, "simpl eq" (assuming no maximal implicit args in
eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed.
By the way, is "mul" on nat defined optimally? "3*n" simplifies to
"n+(n+(n+0))". Are there some advantages of this compared to have it
simplified to "n+n+n" (i.e. to "(n+n)+n").
|
|
|
|
|
|
|
|
|
|
introduction patterns).
Whether we call -> and <- from assert as or apply in as, or as a
component of a larger introduction pattern, the new documented
semantics is:
- behave as subst if an equation rewriting a variable (rewrite in
conclusion and hyps and erase variable and hyp).
- rewrite in concl if an equation not rewrite a variable or a
quantified equality, then erase the hypothesis.
This is potential source of incompatibilities.
|
|
Closes #3761.
|
|
|
|
Commit 3e972b3ff8e532be233f70567c87512324c99b4e renamed coq.el,
coq-db.el, coq-syntax.el to gallina.el, gallina-db.el,
gallina-syntax.el without fixing up any of the references. Commit
30b58d43e48569afb50a35d3915ec7d453a61f5d only fixed up some of them.
Here are some more (hopefully all of them).
Signed-off-by: Anders Kaseorg <andersk@mit.edu>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.
|
|
|
|
|
|
|
|
|
|
|
|
Schemes] option.
|
|
|
|
|
|
|
|
|
|
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
I'm not quite sure why, but I'm pretty sure it's not. Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".
I haven't touched the older instances of it in the CHANGES file.
|
|
"pat/term" for "apply term on current_hyp as pat".
|
|
Isolating a core tactic in replace, shareable to cutrewrite.
|
|
|
