| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
| |
the return clause of match is printed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12480 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
not just type class applications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12479 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
discharged on the other definitions in the section.
- Avoid universe problem in generalize_eqs were we could give an
[@eq_refl Set x x] proof where an [@eq Type x x] was expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Since length and app were defined inside a Section in List.v,
their type argument A wasn't inside the fixpoint. Restoring
the initial definition repairs (at least) Cachan/IntMap.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12477 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- NStrongRec provides a "strong" recursor based on the usual one:
recursive calls can be done here on any lower value.
See binary log in NDefOps for an example of use.
- NDefOps contains alternative definitions of usual operators
(add, mul, ltb, pow, even, half, log)
via usual or strong recursor, and proofs of correctness and/or
of equivalence with axiomatized operators.
These files were in the archive but not being compiled,
some proofs of correction for functions defined there were missing.
By the way, some more iff-style lemmas in Bool.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Correct backtracking function of coqdoc to handle the _p fields of lexers
- Try a better typesetting of [[ ]] inline code considering it as
blocks and not purely inline code like [ ] escapings.
- Rework latex macros for better factorization and support external
references in pdf output.
- Better criterion for generalization of variables in dependent
elimination tactic and better error message in [specialize_hypothesis].
- In autounfold, don't put the core unfolds by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
J'ai ajouté une option '-force-caml-version' au ./configure pour
passer outre la vérification de la version de OCaml. La barre a été
mise à 3.09.3 parce que Khepri (Debian Etch = oldstable) continue de
faire tourner le bench en utilisant OCaml 3.09.3.
Pour info, Coq 8.2 compile avec la 3.08.4, mais pas le trunk.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12473 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Ajout d'un test d'existence de pngtopnm et de pnmtops dans le
./configure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12471 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12469 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
|
|
|
|
|
|
| |
currently supported.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12466 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12465 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
TODO: finish removing the "Add Relation", "Add Morphism" fun_* fun2_*
TODO: now that we have Include, flatten the hierarchy...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12464 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This way we get properties of Rmin / Rmax (almost) for free.
TODO: merge Rbasic_fun and Rminmax...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12463 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12462 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- A richer OrderedTypeFull interface : OrderedType + predicate "le"
- Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
- By the way: as suggested by S. Lescuyer, specification of compare is
now inductive
- GenericMinMax: axiomatisation + properties of min and max out of
OrderedTypeFull structures.
- MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
with also some domain-specific results, and compatibility layer
with already existing results.
- Some ML code of plugins had to be adapted, otherwise wrong "eq",
"lt" or simimlar constants were found by functions like coq_constant.
- Beware of the aliasing problems: for instance eq:=@eq t instead of
eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
instead of Z in statement of Zmax_spec).
- Some Morphism declaration are now ambiguous: switch to new syntax
anyway.
- Misc adaptations of FSets/MSets
- Classes/RelationPairs.v: from two relations over A and B, we
inspect relations over A*B and their properties in terms of classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
(rewrote it differently to avoid being trapped again).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
ForallPairs, etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12459 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Indeed, since sqrt is a total function, most lemmas are true, even for
negative inputs. For instance, sqrt_le_1 was
0 <= x -> 0 <= y -> x <= y -> sqrt x <= sqrt y
while sqrt_le_1_alt is just
x <= y -> sqrt x <= sqrt y.
Naming is done by adding _alt suffixes. In an ideal world (Coq 9.0?), these
new lemmas should just replace the original ones.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12457 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12456 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
like ring)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12454 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12453 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This allows easier handling of dependencies, for instance RelationClasses
won't have to requires List (which itself requires part of Arith, etc).
One of the underlying ideas is to provide setoid rewriting in Init someday.
Thanks to some notations in List, this change should be fairly transparent
to the user. For instance, one could see that List.length is a notation for
(Datatypes.)length only when doing a Print List.length.
For these notations not to be too intrusive, they are hidden behind an explicit
Export of Datatypes at the end of List. This isn't very pretty, but quite handy.
Notation.ml is patched to stop complaining in the case of reloading the same
Delimit Scope twice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12452 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
time should be back to normal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12451 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12450 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
(building an example that needs it to do).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12449 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12448 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12447 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12445 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12444 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12443 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
like the name they refer to).
Fixing buggy test-suite implicit.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
against many patterns.
Conflicts:
lib/dnet.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 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
|
|
|
|
|
|
|
|
| |
(introduced in r12323).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12438 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12437 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
into a SortLabel None.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12434 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12433 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12432 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12431 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12430 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
now accepted.
+svn:ignore property on folders
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12429 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
variables with syntax:
[Local?|Global] Generalizable Variable(s)? [all|none|id1 idn].
By default no variable is generalizable, so this patch breaks backward
compatibility with files that used implicit generalization (through
Instance declarations for example). To get back the old behavior, one
just needs to use [Global Generalizable Variables all].
Make coq_makefile more robust using [mkdir -p].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Correct discharge/classify/rebuild for instances.
Semantic of Global/Local: local by default in sections, global
by default in modules.
- Fix the discrimination net's handling of type universes, let
the unification do it.
- Correct the typeclass resolution tactic so that when extern tactics
themselves launch class resolution we don't duplicate work.
Problem reported by Arthur Chargueraud.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12427 85f007b7-540e-0410-9357-904b9bb8a0f7
|