| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
| |
in */*/vo.itarget
On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
if you want a partial build, make a specific rule such as theories-light
Beware: these vo.itarget should not contain comments. Even if this is legal
for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
with standard math nomenclature. Also clean up in rewrite.ml4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12094 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
unplugged a long time ago.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11798 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
- New functions: update (a kind of union), restrict (a kind of inter),
diff.
- New predicat Partition (and Disjoint), many results about Partition.
- Equivalence instead of obsolete Setoid_Theory (they are aliases).
refl_st, sym_st, trans_st aren't used anymore and marked as obsolete.
- Start using Morphism (E.eq==>...) instead of compat_...
This change (FMaps only) is incompatible with 8.2betaX, but it's really
better now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
only relevant hypotheses in it, slightly cutting the search space.
Makes setoid_rewrite less sensitive to the number of hypothesis (~ 5%
time improvment on the stdlib). This currently prevents resolution with
constants which reduce to classes, hence the modifications in Setoids.Setoid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11360 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
relf/sym/trans relations from morphisms on prop connectives and
relations.
- Add general order theory on predicates, instantiated for relations.
Derives equivalence, implication, conjunction and disjunction as
liftings from propositional connectives. Can be used for n-ary
homogeneous predicates thanks to a bit of metaprogramming with lists of
types.
- Rebind Setoid_Theory to use the Equivalence record type instead of
declaring an isomorphic one. One needs to do "red" after constructor to
get the same statements when building objects of type Setoid_Theory, so
scripts break.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10765 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
symmetric... classes for now, merging Relations with RelationClasses
requires some non-trivial changes on implicits but also some definitions
are different (e.g. antisymmetric in Classes is defined w.r.t an
equivalence relation and not eq). Move back to Reflexive and so on.
reflexivity-like tactics fail in the same way as before if Setoid was
not imported. There is now a scope for morphism signatures, hence "==>",
"++>" and "-->" can be given different interpretations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10708 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from
svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses
........
r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line
Comment grammar error
........
r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines
The initial Type Classes patch.
This patch introduces type classes and instance definitions a la Haskell.
Technically, it uses the implicit arguments mechanism which was extended a bit.
The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters.
It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac).
........
r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line
Fix interface
........
r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line
Fix more xlate code
........
r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines
Update coqdoc for type classes, fix proof state not being displayed on Next Obligation.
........
r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines
Bug fixes in Instance decls.
........
r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines
Streamline typeclass context implementation, prepare for class binders in proof statements.
........
r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line
Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions
........
r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines
Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context.
........
r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line
Stupid bug
........
r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line
Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints
........
r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line
Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors
........
r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines
Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent.
New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental.
Other bugs related to naming in typeclasses fixed.
........
r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines
Progress on setoids using type classes, recognize setoid equalities in hyps better.
Streamline implementation to return more information when resolving setoids (return the results setoid).
........
r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line
Syntax change, more like Coq
........
r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line
Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax
........
r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines
Work on type classes based rewrite tactic.
........
r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines
Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets.
........
r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line
Forgot to add a file
........
r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines
Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and
implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts.
........
r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines
Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations.
Add useful tactics to Program.Subsets.
........
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10150 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10147 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
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
|
| |
|
|
|
|
| |
'properties' de Subversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8082 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4522 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
|
Maxime Dénès
Guillaume Melquiond
herbelin
letouzey
glondu
msozeau
notin
barras
sacerdot
clrenard