| Commit message (Collapse) | Author | Age |
... | |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Deactivation of short names registration and printing for
abbreviations to identical names, what avoids printing uselessly
qualified names binding where the short name is in fact equivalent.
- New treatment of abbreviations to names: don't insert any maximally
inserted implicit arguments at all at the time of the abbreviation
and use the regular internalization strategy to have them inserted
at use time.
- The previous modifications altogether make redirections of
qualified names easier and avoid the semantic change of r12349 and
hence allows to keep "Notation b := @a" as it was before, i.e. as a
notation for the deactivation of the implicit arguments of a.
- Took benefit of these changes and updated nil/cons/list/app
redefinition in "List.v".
- Fixed parsing/printing notation bugs (loop on partially applied
abreviations for constructors in constrintern.ml + bad reverting of
notations with holes that captured non anonymous variables in
match_cases_pattern).
- Add support for parsing/printing abbreviations to @-like constructors
and for reverting printing for abbreviations to constructors applied
to parameters only (function extern_symbol_pattern).
- Minor error messages fixes and minor APIs cleaning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Cleaning and uniformisation in command.ml:
- For better modularity and better visibility, two files got isolated
out of command.ml:
- lemmas.ml is about starting and saving a proof
- indschemes.ml is about declaring inductive schemes
- Decomposition of the functions of command.ml into a functional part
and the imperative part
- Inductive schemes:
- New architecture in ind_tables.ml for registering scheme builders,
and for sharing and generating on demand inductive schemes
- Adding new automatically generated equality schemes (file eqschemes.ml)
- "_congr" for equality types (completing here commit 12273)
- "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
"_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
rewriting schemes (warning, rew_forward_dep cannot be stated following
the standard Coq pattern for inductive types: "t=u" cannot be the
last argument of the scheme)
- "_case", "_case_nodep", "_case_dep" for case analysis schemes
- Preliminary step towards discriminate and injection working on any
equality-like type (e.g. eq_true)
- Restating JMeq_congr under the canonical form of congruence schemes
- Renamed "Set Equality Scheme" into "Set Equality Schemes"
- Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
- Activation of the automatic generation of boolean equality lemmas
- Partial debug and error messages improvements for the generation of
boolean equality and decidable equality
- Added schemes for making dependent rewrite working (unfortunately with
not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Fixed pretty printing of record syntax.
Allowed record syntax inside patterns. (Patch by Cedric Auger.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
implicit arguments and scope (use Implicit Arguments or Arguments
Scope commands instead if not the desired behaviour).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12439 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
- Clarification and documentation of the different styles of
Local/Global modifiers in vernacexpr.ml
- Addition of Global in sections for Open/Close Scope.
- Addition of Local for Ltac when not in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
in Relation_Operators.v and Operators_Properties.v more uniform in
general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12381 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This allow in particular to write eq instead of (@eq _) in
signatures of morphisms. I dont really see how this could
break existing code, no change in the stdlib was mandatory.
We'll check the contribs tomorrow...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
against the incompatibilities introduced by making "destruct" working
on dependent propositions (incompatibilities come from uses of
destruct in Ltac definitions such as "destruct_conjs").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12367 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12347 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
interpreted as using the collection of their constructors as hints.
- Add support for both "using" and "with" in "firstorder". Made the
syntax of "using" compatible with the one of "auto" by separating
lemmas by commas. Did not fully merge the syntax: auto accepts
constr while firstorder accepts names (but are constr really useful?).
- Added "Reserved Infix" as a specific shortcut of the corresponding
"Reserved Notation".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
ExternalProvers.tex in revision 12320.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12324 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r,
Rmult_le_reg_r (mirrored variants of the existing _l lemmas);
- minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs);
- Rle_abs (RRle_abs);
- Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
gappa has been supported for some time in an external package.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12320 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
by Chris Casinghino).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
is true. E.g. "decide (eq_nat_dec n 0) with H" on
H: n=0 |- (if eq_nat_dec n 0 then 1 else 2) = 1
returns
H: n=0 |- 1 = 1 .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq
(maybe an option would be better??).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The compare functions are still functions-by-tactics, but now their
computational parts are completely pure (no use of lt_eq_lt_dec in
nat_compare anymore), while their proofs parts are simply calls
to (opaque) lemmas. This seem to improve the efficiency of sets/maps,
as mentionned by T. Braibant, D. Pous and S. Lescuyer.
The earlier version of nat_compare is now called nat_compare_alt,
there is a proof of equivalence named nat_compare_equiv.
By the way, various improvements of proofs, in particular in Pnat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12247 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12173 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
revealed a too strict test for detection of inferable metas in
Clenv. Restored tolerance for unbound names in interactive tactic use.
- Moral removals of some captures of Not_found in Environ.evaluable_* since
kernel is assumed to deal with existing names.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
reorganization of code) and documentation (in pcoq.mli) of the code
for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
Notation, Notation); merged the two copies of interp_entry_name to
avoid they diverge.
- Added support in Tactic Notation for ne_..._list_sep in general and
for (ne_)ident_list(_sep) in particular.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
in both files. Late update of CHANGES wrt classical Tauto.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12084 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
argument is a variable bound to a list (see S. Lescuyer's message on
coq-club, Apr 5, 2009).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12050 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12040 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
is not so robust).
- Updating CHANGES
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12008 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11962 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11944 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
...and use -custom by default on Windows and MacOS (backport r11895)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11913 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11862 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Updated CHANGES.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11747 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11730 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
identity. Add notations for compatibility and support for
understanding these notations in the ml files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
the naming of hypotheses (especially when doing "case H" with H of
type "{x|P<->Q}" since not unfolding will eventually introduce a name
"i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
of names manipulating type constr_pattern, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
of the archive to install in coq user-contrib installation directory.
- Relaxed the validity check on identifiers from an error to a warning.
- Added a filtering option to Print LoadPath.
- Support for empty root in option -R.
- Better handling of redundant paths in ml loadpath.
- Makefile's: Added target initplugins and added initplugins to coqbinaries.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
DecidableType
After lots of hesitations, OrderedType now requires this "eq_dec" field, which
is redundant (can be deduced from "compare"), but allows the subtyping relation
DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly
extensions of weak sets. Of course this change introduces a last-minute
incompatibility, but:
- There is a clear gain in term of functionnality / simplicity.
- FSets 8.2 already needs some adaptations when compared with 8.1, so it's
the right time to push such incompatible changes.
- Transition shouldn't be too hard: the old OrderedType still exists under
the name MiniOrderedType, and functor MOT_to_OT allows to convert from
one to the other.
Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType
(resp. OrderedType), an eq_dec on sets is now required in these interfaces
and in the implementations. In pratice, it is really easy to build from
equal and equal_1 and equal_2.
Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun,
while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M).
Idem with WDecide, WProperties and WEqProperties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11690 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Added "simple apply in" (cf wish 1917) + conversion and descent
under conjunction + contraction of useless beta-redex in "apply in"
+ support for open terms.
- Did not solve the "problem" that "apply in" generates a let-in which
is type-checked using a kernel conversion in the opposite side of what
the proof indicated (hence leading to a potential unexpected penalty
at Qed time).
- When applyng a sequence of lemmas, it would have been nice to allow
temporary evars as intermediate steps but this was too long to implement.
Smoother API in tactics.mli for assert_by/assert_as/pose_proof.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11662 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11620 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
slight improving of the printing of record.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11619 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
revival of option -translate as a -beautify option.
PS: compilation checked against 11610.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11618 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CoInductive stream (A:Type) := { hd : A ; tl : stream A }.
Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }.
L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de
la syntaxe qui était apparue dans la 8.2beta pour les records
coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive"
comme maintenant).
VernacRecord et VernacInductive semblent maintenant faire doublon, il
doit y avoir moyen de les fusionner.
Les records mutuellement inductifs restent aussi à faire.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11523 85f007b7-540e-0410-9357-904b9bb8a0f7
|