| Age | Commit message (Collapse) | Author |
|---|
|
elimination scheme in induction/destruct also for those names which
correspond to neither the induction hypotheses nor the recursive
arguments.
|
|
|
|
|
|
|
|
-I is (only) the ml one
-I -as is fixed
-Q is understood
-R is not a recursive ml include anymore
$COQENV, user_contrib, ... are not recursively included
coqlib/theories and coqlib/plugins are still recursively included (for now). (This
may deserves an option)
Closes Bug 2910: If there is a "Require a." in a b.v and a a.vo in path but no a.v,
coqdep does not complains about a missing a.v.
|
|
|
|
variable
as algebraic so it can disappear from the proof (it always gets substituted away from
the term). This means less spurious universes remaining in proof terms.
|
|
reductions in
case the constant was hiding a direct match for example. Also avoid two lookups
of ReductionBehavior per constant application in simpl.
|
|
its universe doesn't get constrained unnecessarily (bug found in MathClasse).
Also avoid using rewrite itself in a proof in Morphisms.
|
|
|
|
or-and intropatterns bind a limited number of patterns: if * or ** are
used, the bound has to be used (since there is no heavy compatibility
to respect for * and **). This fixes test-suite/success/intros.v.
|
|
a global reference that the current (goal) env contains all the
section variables that the global reference expects to be present.
Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.
It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.
Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)
or
Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True. (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)
|
|
into a specific new cleaned file find_subterm.ml.
This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
|
|
not a variable, in the future objective to factorize code between
"generalize dependent" and "set", "destruct", etc.
|
|
proof engine. Moved it to unification.ml.
|
|
|
|
|
|
|
|
|
|
form of a potential canonical argument anymore, and we check that it may be part
of a canonical structure first.
|
|
Fixes the behavior of reflexivity/symmetry etc... when Setoid is not loaded.
|
|
|
|
|
|
|
|
|
|
|
|
incompatibilities, at least until the check of compilation of contribs
succeeds more often.
Incidentally adapted some proofs in Reals which were not agnostic
relatively to whether the option is on or off.
|
|
|
|
|
|
is has non-local effects. For now it is not disabled by default, but we'll
try to disable it once the test-suite and contribs are stabilized.
|
|
JasonGross-tc
|
|
|
|
|
|
|
|
the hypotheses in eauto.
|
|
|
|
|
|
|
|
JasonGross-more-test-suite
Conflicts:
test-suite/bugs/closed/3300.v
test-suite/bugs/closed/3373.v
|
|
|
|
|
|
|
|
as this would result in an ill-scoped substitution.
|
|
the computed direction argument. In case pbty is conv, no refreshing is done
as the evar body must be convertible with the given term, however refreshing
of template application evar arguments can still happen.
(Re)-Closing bug #2966.
|
|
|
|
|
|
correct constraints (bug found in CFGV).
|
|
generated an uncaught Not_found. This raises an anomaly now and the sort is
properly computed now (fixes a bug in CoLoR).
|
|
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
User interface writers can drop a footop.cmxs in $(COQLIB)/toploop/
and pass -toploop footop to customize the coq main loop.
A toploop must set Coqtop.toploop_init and Coqtop.toploop_run to
functions respectively initializing the toploop (and parsing toploop
specific arguments) and running the main loop itself.
For backward compatibility -ideslave and -async-proofs worker do
set the toploop to coqidetop and stmworkertop respectively.
|
