| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
1. when applying a functor F(X) := B to a module M, the obtained module
is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the
body of t in M}. In principle it is now easy to fine tune the behaviour
to choose whether b or M.t must be used. This change implies modifications
both inside and outside the kernel.
2. for each object in the library it is now necessary to define the behaviour
w.r.t. the substitution {X.t := b}. Notice that in many many cases the
pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken
(in the sense that it used to break several invariants). This commit
fixes the behaviours for most of the objects, excluded
a) coercions: a future commit should allow any term to be declared
as a coercion; moreover the invariant that just a coercion path
exists between two classes will be broken by the instantiation.
b) global references when used as arguments of a few tactics/commands
In all the other cases the behaviour implemented is the one that looks
to me as the one expected by the user (if possible):
[ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ]
a) argument scopes: not expanded
b) SYNTAXCONSTANT: expanded
c) implicit arguments: not expanded
d) coercions: expansion to be done (for now not expanded)
e) concrete syntax tree for patterns: expanded
f) concrete syntax tree for raw terms: expanded
g) evaluable references (used by unfold, delta expansion, etc.): not
expanded
h) auto's hints: expanded when possible (i.e. when the expansion of the
head of the pattern is rigid)
i) realizers (for program extraction): nothing is done since the actual
code does not look for the realizer of definitions with a body;
however this solution is fragile.
l) syntax and notation: expanded
m) structures and canonical structures: an invariant says that no
parameter can happear in them ==> the substitution always yelds the
original term
n) stuff related to V7 syntax: since this part of the code is doomed
to disappear, I have made no effort to fix a reasonable semantics;
not expanded is the default one applied
o) RefArgTypes: to be understood. For now a warning is issued whether
expanded != not expanded, and the not expanded solution is chosen.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6323 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
the CVS working dir)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3573 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
noms uniques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
gregoire
sacerdot
barras
herbelin
coq