| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
n'est pas assez puissante pour retarder la coercion vers le but au dernier moment
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
* the Unfold hints of auto/eauto now use evaluable_global_references in place
of global_references
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6428 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6427 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6426 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
avec l'environnement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6424 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
envoie à refine des métas castées avec des métas ?!)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6422 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
changement de CastedOpenConstr en OpenConstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6419 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
que de fonctions récursives même si l'une de ses fonctions n'a pas de meta); suppression gmm au passage suite commit précédent
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6418 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
tactiques d'appliquer une éventuelle coercion vers le but
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6407 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
camlp4-generated code even if it is not found using grep)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6351 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6350 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
compatibilité avec Write State
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6339 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6335 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
the new module kernel/mod_subst.ml.
MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now
possible to define substitutions that also delta-expand constants
(by associating the delta-expanded form to the constant name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.
KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
la doc (la forme 'with' du premier a été cassé dans la version 1.3 de leminv.ml (V7.0), tandis que la forme sans 'with' et le second étaient déjà cassés dans la V6.2)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6300 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
A rule is a duplicate of another rule when their types are alpha convertible.
Eliminating duplicates speed up the tactic (but it slows down the operation
of addition of a new rule that is also performed every time subst_mps is applied
to the module).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6263 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6262 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
factorisation cut_replacing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6261 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6255 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6253 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
types. Fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6249 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6248 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Closed again.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6243 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@6237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
a quantified Leibniz relation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6236 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
became the whole structure of type Morphism_Theory. A new field morphism_theory
has now been added to record both informations. Print Setoids now prints again
the right information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
order (and thus they were not accepted).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6234 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
goal with metavariables in it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6233 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
definitions in their types are now accepted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6232 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
relation/morphisms are quantified using LetIns.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6222 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
is now the one that is shown to the user (and not only convertible to it).
In this way it is possible to register the lemma in the Hint database.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
existential variables it failed. Fixing by propagating the metavariable
environment generated by the unification.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6215 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6214 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
to their setoid_* counterparts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6213 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6211 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
evaluation of tactics
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6194 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
setoid_reflexivity
setoid_symmetry
setoid_transitivity
The command
setoid_symmetry in ...
is not implemented yet (it behaves just as symmetry in ... for now).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6193 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6191 85f007b7-540e-0410-9357-904b9bb8a0f7
|