| Age | Commit message (Collapse) | Author |
|---|
|
with -R. (Fix for Rocq/Rational.)"
This reverts commit 7d3ce4012a53b123dac95381bf46aac65f865d69.
Conflicts:
CHANGES
|
|
This option complements -I-as and -R. As the two other options, it adds a
new loadpath, but contrarily to them, files are not looked into the
directory unless fully qualified.
|
|
(Fix for Rocq/Rational.)
|
|
- Option -I no longer handles loadpath, only mlpath. This is the same
behavior as coq_makefile. Option -I-as is unchanged.
- Option -R no longer recursively adds to mlpath; only the root directory
is added.
- user-contrib/ and xdg directories are no longer recursively added to
the loadpath.
- theories/ and plugins/ are no longer recursively added to the loadpath
when option -nois is passed.
- All the preconfigured directories are still recursively added to the
mlpath though.
|
|
NB: Please re-run ./configure after pulling this commit
For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore,
but rather CUnix.sys_command, which is based on Unix.create_process.
This way, we do not need to bother with the underlying shell
(/bin/sh or cmd.exe) and the way arguments are to be quoted :-).
Btw, many cleanups of coqmktop.
Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option"
that collect as a string several sub-options to be given by coqmktop to ocamlc.
For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to
parse all these sub-options. To ease that, I've made the following changes
to the ./configure options:
* The -coqrunbyteflags and its blank-separated argument isn't accepted
anymore, and is replaced by a new option -vmbyteflags which expects
a comma-separated argument. For instance:
./configure -vmbyteflags "-dllib,-lcoqrun"
Btw, on this example, the double-quotes aren't mandatory anymore :-)
* The -coqtoolsbyteflags isn't accepted anymore. To the best of my
knowledge, nobody ever used it directly (it was internally triggered
as a byproduct of the -custom option). The only interest I can think of
for this option was to cancel the default use of ocamlc custom-linking
on Win32 and MacOS. For that, ./configure now provides a -no-custom option.
|
|
|
|
Omega now reuse the same inner variable names (Zvar0, Zvar1, ...)
at each run. This way, the obtained proof-terms on
two identical omega runs should be the same.
This wasn't always the case earlier:
- the two proofs were almost always convertible, but with distinct
variable names.
- in very rare situations, the two proofs could even be non-convertible.
Indeed, the omega engine use hash-tables which may be sensible to
the names in the (in)equality system and hence lead to different
solutions. Example of this behavior (with ocaml 4, whose default hash
function is different from ocaml 3.12, leading to a different behavior
here !) :
--------------------------------------------------------------------
Require Import Omega.
Lemma test1 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test2 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test3 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Lemma test4 : forall i j, i < j -> i-1 < j. intros; omega. Defined.
Check (eq_refl : test1 = test2). (* OK *)
Check (eq_refl : test1 = test3). (* OK *)
Check (eq_refl : test1 = test4). (* KO, test4 is different !! *)
--------------------------------------------------------------------
The old behavior could be restored with "Unset Stable Omega".
Thanks to Frédéric Loulergue for spotting this sensibility to
the underlying ocaml versions...
|
|
|
|
Since digests are strings (of size 16), we just dump them
now in vo files (cf. Digest.output) instead of using Marshal
on them : this is cleaner and saves a few bytes.
Increased VOMAGIC to clearly identify this change in the format.
Please rerun ./configure after this commit.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly
Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.
However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
"injection" tactic when applied on an equality statement. Moreover,
hypotheses are now entered in the left-to-right order.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16539 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
occurrences (possible source of incompatibilities since this alters
the numbering of occurrences).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16525 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
the form "_ pat1 ... patn", and considering it experimental at this
stage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16466 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
I hope I did not forget any place to change.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Added full betaiota in hnf. This seems more natural, even if it
changes the strict meaning of hnf. This is source of incompatibilities
as "intro" might succeed more often.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
reduced in order to find some head constant to reduce.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
has to be refered through its qualified name even when the module
containing it is imported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
error. Maybe displaying environment is making output overly verbose,
but this can also be considered an IDE issue, which would e.g. provide
a button to hide/display environment of the error message...
Also added some "make_all_name_different" which should probably
prevent some anomalies "index to an anonymous variable" at error
reporting time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16208 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
notations: - hopefully never 2 spaces when the user did not ask for -
more systematic default insertion of spaces around symbols - e.g. have
space before "[" if after a non-terminal - have spaces between
consecutive terminals
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15730 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15672 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:
destruct x eqn:H
destruct x as [ ] eqn:H
Some with induction. Of course, the pattern behind "as" is arbitrary.
For an anonymous version, H could be replaced by ?. The old syntax
with "_eqn" still works for the moment, by triggers a warning.
For making this new syntax work, we had to change the seldom-used
"induction x y z using foo" into "induction x, y, z using foo".
Now, only one "using" can be used per command instead of one per
comma-separated group earlier, but I doubt this will bother anyone.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
So -> is at level 99 since commit 15515. In particular it has now
*less* priority than <->, i.e. A->B<->C is now parsed as A->(B<->C)
instead of the former awkward and beginner-misleading (A->B)<->C.
Sorry, I was planning to do a separate commit for that, but I forgot.
In fact, the parsing rules for -> were slightly changed during
Pierre B's recent conversion of -> to a true Notation, leading
to a nasty sitution : A->B<->C->D was parsed as A->(B<->(C->D)).
With no obvious solution to restore full compatibility, we decided
to go for the parsing described above, both easy to implement
and to work with.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15523 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15426 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15393 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15357 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Let's check tomorrow the impact on contribs: are the recent build
failures related to the "not" unfolding stategy or to the new
handling of conjonction-like constructors ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15330 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Why2 has not been maintained for the last few years and the Why3 plugin should
be a suitable replacement in most cases.
Removed tactics: simplify, ergo, yices, cvc3, z3, cvcl, harvey, zenon, gwhy.
Removed commands: Dp_hint, Dp_timeout, Dp_prelude, Dp_predefined, Dp_debug,
Dp_trace.
Note that the "admit" tactic was actually provided by the Dp plugin. It has
been moved to extratactics.ml4.
Ported from v8.4 r15186.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15189 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- tauto/intuition now works uniformly on and, prod, or, sum, False,
Empty_set, unit, True (and isomorphic copies of them), iff, ->, and
on all inhabited singleton types with a no-arguments constructor
such as "eq t t" (even though the last case goes out of
propositional logic: this features is so often used that it is
difficult to come back on it).
- New dtauto and dintuition works on all inductive types with one
constructors and no real arguments (for instance, they work on
records such as "Equivalence"), in addition to -> and eq-like types.
- Moreover, both of them no longer unfold inner negations (this is a
souce of incompatibility for intuition and evaluation of the level
of incompatibility on contribs still needs to be done).
Incidentally, and amazingly, fixing bug #2680 made that constants
InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto
had indeed destructed a section hypothesis "@StrictOrder A ltA@
thinking it was a conjunction, making this section hypothesis
artificially necessary while it was not.
Renouncing to the unfolding of inner negations made auto/eauto
sometimes succeeding more, sometimes succeeding less. There is by the
way a (standard) problem with not in auto/eauto: even when given as an
"unfold hint", it works only in goals, not in hypotheses, so that auto
is not able to solve something like "forall P, (forall x, ~ P x) -> P
0 -> False". Should we automatically add a lemma of type "HYPS -> A ->
False" in the hint database everytime a lemma ""HYPS -> ~A" is
declared (and "unfold not" is a hint), and similarly for all unfold
hints?
At this occasion, also re-did some proofs of Znumtheory.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15179 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial contribution by Andrew Appel, many ulterior modifications
by myself.
Interest: red-black trees maintain logarithmic depths as AVL,
but they do not rely on integer height annotations as AVL,
allowing interesting performance when computing in Coq or after
standard extraction. More on this topic in the article by A. Appel.
The common parts of MSetAVL and MSetRBT are shared in a new file
MSetGenTree which include the definition of tree and functions
such as mem fold elements compare subset.
Note that the height of AVL trees is now the first arg of the
Node constructor instead of the last one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15130 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
To mitigate the lack of a general "info" tactical, let's
introduce some specialized tactics info_trivial, info_auto
and info_eauto that display the basic tactics used when
solving a goal.
We also add tactics "debug trivial" and "debug auto" which
display every basic tactics attempted by trivial or auto.
Triggering the "info" or "debug" mode for auto, eauto, trivial
can also be done now via global options, such as Set Debug Auto
or Set Info Eauto. In case both debug and info modes are
activated, the debug mode takes precedence.
NB: it would be nice to name these tactics "info xxx" instead
of "info_xxx", but I don't see how to implement a "info eauto"
in eauto.ml4 (hence by TACTIC EXTEND) while keeping
a generic "info foo" tactic in g_ltac.ml4 (useful to display
a nice message about the unavailability of the general info).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
longer be bound to Funclass or Sortclass (this does not seem to be
useful). [An exception is when using modules, if a constant foo is
expanded into a type, a "Bind Scope sc with foo" starts binding
Sortclass].
Also reworked reference manual for Arguments Scopes and Bind Scopes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We now accept the following code: Definition E := 0. Module E. End E.
Techically, we simply allow the same label to occur at most twice in
a structure_body, which is a (label * structure_field_body) list).
These two label occurences should not be at the same level of fields
(e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or
a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change.
Drawback : no more simple List.assoc or equivalent should be performed
on a structure_body ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15086 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- (Regular) Casts become typing constraints again.
- Coerce tycon to inductive type when applying bidirectional typechecking hint.
- Coerce lambda expressions to tycon, might require coercions now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15058 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- reinstall (x : T | P) binder syntax extension.
- fix a wrong Evd.define in coercion code.
- Simplify interface of eterm_obligations to take a single evar_map.
- Fix a slightly subtle bug related to resolvability of evars: some
were marked unresolvable and never set back to resolvable across calls
to typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
call to "idtac foo" in Ltac code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14929 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
printing) of implicit arguments (a priori useful for teaching).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
|
