| Age | Commit message (Collapse) | Author |
|---|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
sig, sig2, sumor, list et vector dans Type
- Branchement de prodT/listT vers les nouveaux prod/list
- Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2
- Changements en conséquence dans les théories (notamment Field_Tactic),
ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Du coup, factorisation d'une partie dans SetoidList. Ajout de
lemmes suggeres par Evelyne C. Un oubli dans FSetWeakInterface
concernant elements.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8804 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6306 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6241 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
duplicated between add_relation and add_setoid.
* Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v
* Term size reduction (first part): when a relation is registered, we add
to the environment a definition that gives back either the relation as
an argument or as a relation class. The definition is used to reduce
the term size. [ Note: we could save a bit more by defining two definitions
in place of one. However, we suppose that the lambda term fragments generated
can be shared quite effectively. Thus we would recive almost no benefit by
sharing in terms of size. What about proof checking time? ]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6192 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
now declares both the relation and the relation as a morphism, computing
the appropriate signature (depending on the reflexivity of the relation).
* New parameter "as ..." to Add Relation (to be able to compute the
morphism name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6188 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6154 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6153 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* reuse of definitions already given in the standard library
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
irreflexive relations (in particular partial setoids, also called
typoids). This feature was asked by Marco Maggesi.
The Coq part of the tactic has now reached the planned expressive power.
However, the ML part does not exploit yet the full expressiveness.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
asymmetric relations thanks to the introduction of morphisms that are
covariant or contravariant in their arguments.
* The ML part of the tactic is updated only for backward compatibility: it
is still not possible to benefit from the asymmetric relations and relative
morphisms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6070 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
introduces a few backward incompatibilities:
1. setoid_replace used to try to close the new goal using full_trivial.
The new implementation does not try to close the goal.
To fix the script it is sufficient to add a "; [ idtac | trivial ]."
after every application of setoid_replace that used to generate just
one goal.
2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1
(if c1 did not occur in the goal). The new implementation only replaces
c1 with c2.
To fix the script it is sufficient to replace
(setoid_replace c1 with c2) with
(setoid_replace c1 with c2) || (setoid_replace c2 with c1)
in those cases where it is unknown what should be substituted with what.
3. the goal generated by the "Add Morphism" command has the hypothesis
permutated w.r.t. the old implementation. I.e. the old implementation
used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ...
whereas the new implementation generates
forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ...
Fixing the script is usually trivial.
4. the "Add Morphism P" command used to generate a non-standard goal in the
case of P being a predicate (i.e. a function whose codomain is Prop).
In that case the goal ended with an implication (instead of ending with
a coimplication). The new implementation generates a standard goal that
ends with a coimplication.
To fix the script you can add the following line at the very beginning:
cut <<old_goal>>; intro Hold; split; apply Hold;
assumption || (symmetry;assumption).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2731 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1992 85f007b7-540e-0410-9357-904b9bb8a0f7
|
