| Age | Commit message (Collapse) | Author |
|---|
|
|
|
with Enrico.
|
|
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
|
We purge the environment given to the morphism searcher from all dependencies
on the considered variable. I hope it is not too costly.
|
|
|
|
of temporary hypotheses than 76f27140e6e34 did.
|
|
of "apply ... in ... as ..." in the context.
Fixing a regression done by 7e00e8d60 and f2130a88e1: when an evar is
created, the statement of the refined hypothesis virtually depends on
the whole context and has to be left at the top.
|
|
... lemmas and inductives to control which universes are bound and where
in universe polymorphic definitions. Names stay outside the kernel.
|
|
Namely, it accepts, variables, constants, inductives and constructors.
When these have a qualified name, the fresh is done on its basename.
|
|
|
|
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.
|
|
|
|
|
|
compatibility with the non uniform behavior that "intros [] []" on
"A*B->C*D->E" automatically introduces A and B but leaves C and D in
the goal.
Kept unset in 8.5 but planned to be set in 8.6.
|
|
|
|
to behave like "specialize (H ...)" since 4/8/2008 (r11300, 7d515acbc5).
|
|
Grants wish #2098.
|
|
|
|
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
|
in 8.4 with the schemes of the subcomponent of an inductive added to
the environment or discharged as let-ins over the main scheme.
As of today, decidable-equality schemes are built when calling
vernacular command (Inductive with option Set Dedicable Equality
Schemes, or Scheme Equality), so there is no need to discharge the
sub-schemes as let-ins. But if ever the schemes are built from within
an opaque proof and one would not like the schemes and a fortiori the
subschemes to appear in the env, the new addition of a parameter
internal_flag to "find_scheme" allows this possibility (then to be set
to KernelSilent).
|
|
considering trivial unifications "?x = t" in tactics working under
conjunctions (see #3545).
Also updating and fixing wrong comments in test apply.v.
|
|
|
|
We postpone the rewriting of hypothesis until we actually commit to one
branch instead of doing it upfront.
|
|
Commit dc438047 was a bit overlooked as it introduced a wrong comparison function
on term patterns in dnets. Strangely enough, it seems not to have wreaked havoc
that much compared to the severity of the error.
|
|
|
|
|
|
Tracing with gdb by Alec Faithfull
|
|
|
|
|
|
maybe ca71714).
Goal 2=2+2.
match goal with |- (_ = ?c) => simpl c end.
was working in 8.4 but was failing in 8.5beta2.
Note: Changes in tacintern.ml are otherwise purely cosmetic.
|
|
|
|
|
|
|
|
|
|
|
|
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
|
|
|
|
|
|
|
Conflicts:
tactics/eauto.ml4
(merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
|
|
Internal error: Anomaly: Uncaught exception Not_found. Please report.
An evarmap was lost because of an unsound typing primitive.
|
|
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
|
It accepts three distinct flags:
- "Lax", which is the default one, sets the old behaviour, i.e. a non-imported
hint behaves the same as an imported one.
- "Warn" outputs a warning when a non-imported hint is used. Note that this is
an over-approximation, because a hint may be triggered by an eauto run that
will eventually fail and backtrack.
- "Strict" changes the behaviour of an unloaded hint to the one of the fail
tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
|
|
|
|
|
|
We beta-iota normalize the type of the rewriting predicate to ensure that the
non-dependency in the arrow argument is meaningful. Otherwise, terms of the
form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse
the non-dependency heuristic.
|
|
|
|
preserving compatibility of subst after #4214 being solved.
|
|
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
|
