| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
out. The semantics of the old setoid are faithfully simulated by the new
tactic, hence no scripts involving rewrite are modified. However,
parametric morphism declarations need to be changed, but there are only a
few in the standard library, notably in FSets. The declaration and the
introduction of variables in the script need to be tweaked a bit,
otherwise the proofs remain unchanged.
Some fragile scripts not introducting their variable names explicitely
were broken. Requiring Setoid requires Program.Basics which sets stronger
implicit arguments on some constants, a few scripts benefit from that.
Ring/field have been ported but do not really use the new typeclass
architecture as well as they could. Performance should be mostly
unchanged, but will certainly improve in the near future. Size of the
vo's seems not to have changed at all.
It will certainly break some contribs using Setoid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
and add a simpler synonym for "exactly N times" :
rewrite 3 H (or rewrite 3H) means rewrite 3!H
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10629 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
binding, add "!" syntax for the new binders which require parameters and
not superclasses. Change backquotes for curly braces for user-given
implicit arguments, following tradition. This requires a hack a la
lpar-id-coloneq. Change ident to global for typeclass names in class
binders. Also requires a similar hack to distinguish between [ C t1 tn ]
and [ c : C t1 tn ]. Update affected theories.
While hacking the parsing of { wf }, factorized the two versions of fix
annotation parsing that were present in g_constr and g_vernac.
Add the possibility of the user optionaly giving the priority for resolve and
exact hints (used by type classes). Syntax not fixed yet: a natural
after the list of lemmas in "Hint Resolve" syntax, a natural after a "|"
after the instance constraint in Instance declarations (ex in
Morphisms.v).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- l'occur-check doit être fait aussi quand on imite,
- pour simplifier et en se basant sur les commentaires antérieurs à
1995 (de Chet?) et parlant de mimick_evar, on restreint l'appel à
mimick_evar au cas où l'instance contient des Meta.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
compiler la contrib Nijmegen/QArith ?!)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10625 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- les erreurs de solve_simple_evar_eqn étaient rattrapées par mégarde,
- à défaut de traitement des conv_pbs dans unification.ml, on évite
d'accumuler des contraintes pour l'instant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10624 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
dans certains cas. Branchement au passage de w_unify vers evar_conv et
solve_simple_eqn en cas d'équations entre Evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
telles que Godel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10622 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
hints arith
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* When no explicit module type is given in Coq, extraction proceeds
with more caution when recontructing a module type from the
module. For instance, a module ident isn't keep, since it's the name
of an implementation, not of a module type. Fix the bug
functor M -> M : funsig M -> M instead of funsig M -> typeof(M)
* Removed duplicated code with Modops
* The call to replicate_msid doesn't seem to be as crucial as before.
Let's try to remove it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10620 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10619 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10618 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10615 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
... but still no idea why it was working fine on some machines
even without this patch...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10614 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
(rapport de bug 1807). Cf explication dans le fichier et/ou dans le
bug-tracker.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10613 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1) changed the semantics of rewrite H,H' : the earlier semantics
(rewrite H,H' == rewrite H; rewrite H') was poorly suited for
situations where first rewrite H generates side-conditions.
New semantics is tclTHENFIRST instead of tclTHEN, that is
side-conditions are left untouched.
Note to myself: check if side-effect-come-first bug of
setoid rewrite is still alive, and do something if yes
2) new syntax for rewriting something many times. This syntax is
shamelessly taken from ssreflect:
rewrite ?H means "H as many times as possible"
(i.e. almost repeat rewrite H, except that
possible side-conditions are left apart as in 1)
rewrite !H means "at least once" (i.e. rewrite H; repeat rewrite H)
rewrite 3?H means "up to 3 times", maybe less
(i.e. something like: do 3 (try rewrite H)).
rewrite 3!H means "exactly 3 times" (i.e. almost do 3 rewrite H).
For instance: rewrite 3?foo, <-2!bar in H1,H2|-*
3) By the way, for a try, I've enabled the syntax +/- as synonyms for
->/<- in the orientation of rewrite.
Comments welcome ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10612 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
que possible des variables qui ont déjà un nom joli tout plein.
La conséquence c'est qu'on peut aussi faire "destruct 0" qui est
vachement moins intéressant... Mais bon.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10610 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Rpower_O alors qu'on la garde pour les autres propriétés de la puissance.
(résultat d'une discussion avec Assia et Jean-Marc)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10609 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
- clarifications about Equality on maps
Caveat: name change, what used to be Equal is now Equivb
- the prefered equality predicate (the new Equal) is declared
a setoid equality, along with several morphisms
- beginning of a filter/for_all/exists_/partition section in FMapFacts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10608 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10605 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10604 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10602 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
The old version is now a properties in FSetProperties.OrdProperties
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10600 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10599 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10597 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10596 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10595 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
#939
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10594 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10593 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10592 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10590 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
(Axiom/Variable...). New tactic clapply to apply unapplied class methods
in tactic mode, simple solution to the fact that apply does not work
up-to classes yet. Add Functions.v for class definitions related to
functional morphisms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10586 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10585 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10584 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10581 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10579 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10578 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10577 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10576 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10575 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10574 85f007b7-540e-0410-9357-904b9bb8a0f7
|