| Age | Commit message (Collapse) | Author |
|---|
|
|
|
108 used an implicit lowering to Prop.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
No universe can be set lower than Prop anymore (or Set).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
of temporary hypotheses than 76f27140e6e34 did.
|
|
|
|
|
|
|
|
ago) which broke compilation of theories/Logic/WKL.v (collision
between a temporary name and a user name).
|
|
an initial hypothesis hyp at the same position in the context.
Ensuring the same for "apply c in hyp as pat".
Ensuring that "pose proof (H ...) as H" does not change the position of H.
|
|
|
|
|
|
"Fetching opaque proofs" notices are not printed by default anymore.
|
|
|
|
|
|
I don't know what was the intent of Pierre B here. In 8.4, it was not
supported, raising with an error at parsing time. I changed the
anomaly into an error at interpretation time, so it is still not
supported but we could support it if some legitimate use of it
eventually appears.
|
|
|
|
This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)). It is
useful to have function_scope for, e.g., function composition. This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.
Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax. (The scope type_scope
should not be special-cased; this change is coming up next.)
Also explicitly define [function_scope] in theories/Init/Notations.v.
This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]
We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.
|
|
|
|
|
|
of syntax in test file ltac.v.
|
|
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
|
|
capturing bound names unexpectingly).
We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").
We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in
let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).
which was producing
forall z : nat, match z with 0 => z | S y => y end = 0
because the names in default branches are treated specifically.
It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).
However, we rename binders in fix which were not interpreted.
There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).
fix ltac name
|
|
considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).
Also updating and fixing wrong comments in test apply.v.
|
|
|
|
breaking backtracking in the presence of functors).
In "interactive" rather than "bugs" because of the use of Back.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
abbreviation not bound to an applied constructor as itself but rather
as a binding variable as it was the case for non-applied
constructor). This was broken by e5c02503 while fixed #3483 (Not_found
uncaught with a notation to a non-constructor).
|
|
decidability scheme).
Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:
Set Decidable Equality Schemes.
Inductive a := A with b := B.
which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
|
