| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit concerns about the first half of the useless code
mentionned by Oug for coqtop (without plugins). For the moment,
Oug is used in a mode where any elements mentionned in a .mli
is considered to be precious. This already allows to detect and
remove about 600 lines, and more is still to come.
Among the interesting points, the type Entries.specification_entry
and its constructors SPExxx were never used. Large parts of cases.ml
(and hence subtac_cases.ml) were also useless.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11595 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11593 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
- compare the integer indexes first, in order to avoid
comparing the dirpath part if possible
- use an ad-hoc comparison function rather than Pervasives.compare
(slightly faster during my tests on the compcert contrib)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11589 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
contraintes bornant par le haut le type de l'inductif (ce qui peut
arriver quand l'inductif est argument d'une constante) étaient
oubliées : on pouvait se retrouver avec des inductifs dont le type des
constructeurs, une fois instancié par des paramètres) n'était plus
typable (seul leur réduit, après expansion des constantes, était
typable). [kernel, test-suite]
+ Affichage des inductifs (via Print) en prenant la forme utilisateur des
constructeurs.
+ Correction warning dans compilation gallina.ml.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11266 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
les notations dans les alias de module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11063 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
univers, suite à discussion avec Bruno : on franchit le cap et on
ajoute le sous-typage Prop <= Set. On n'a donc plus besoin d'utiliser
l'image de Prop dans la hiérarchie en dehors de la zone de calcul de
la sorte la plus basse d'un inductif polymorphe (au passage, nous
avons décidé de renommer Type -1 en Type 0-, pour bien indiquer qu'il
se trouve au même niveau que Type 0).
Coq se retrouve donc avec la hiérarchie Prop <= Set <= Type i et avec
une copie de Prop (Type 0-) et une copie de Set (Type 0) dans la
hiérarchie Type. En théorie, on pourrait donc supprimer "Prop Null" et
"Prop Pos" de l'implémentation et ne travailler qu'avec "Type".
L'ajout de Prop <= Set vaut à la fois dans le cas Set prédicatif et
dans le cas Set imprédicatif (Prop et Set étant en bas de la
hiérarchie, il n'y a pas d'incohérence connue). Dans le modéle
ensembliste, Prop et Type 0- sont interprétés par exemple comme
{{},{o}}, où "o" est un objet particulier interprétant les preuves, et
il n'y a pas de Set imprédicatif. Dans un modèle de réalisabilité,
Set imprédicatif est interprétable et Prop peut au choix s'interpréter
comme Set ou comme booléen (cf la thèse de Miquel). Le sous-typage du
côté ensembliste s'obtient en mettant au moins l'ensemble {{},{o}}
dans l'interprétation de Set (ce qu'on fait de la même manière que
Prop <= Type 1, avec conversion typée), et du côté réalisabilité en
mettant l'ensemble {Typ(vide),Typ(unit)} dans l'interprétation de Set
("Typ" étant la coercion faisant d'un ensemble un terme), ce qui est
fait dans la section 6.2.4 de la thèse d'Alexandre Miquel (modèle du
CC implicite sans types inductifs).
Il reste un problème pratique. Lorsqu'on donne
Inductive unit:Type := tt:unit.
Coq dit que unit est dans Prop. C'est correct parce qu'il n'y a pas de
contraintes d'univers mais un peu déroutant même si la coercion
"unit : Set" reste valide. Une suggestion est de ne rendre polymorphe
que les inductifs dont on ne donne pas la sorte explicitement, comme dans
Inductive unit := tt:unit.
mais alors, comment indiquer l'absence de sorte explicite si le type a
des paramètres réels (comme "vect") ??
PS: modification de sort_cmp dans checker/inductive.ml faite.
--This line, and those below, will be ignored--
M kernel/univ.ml
M kernel/univ.mli
M kernel/inductive.ml
M kernel/reduction.ml
M kernel/indtypes.ml
M checker/inductive.ml
M checker/reduction.ml
M pretyping/reductionops.ml
M pretyping/termops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(i.e. "Inductive unit := tt." conduisait à "t:Prop" alors que le
principe de la hiérarchie d'univers est d'être cumulative -- et que
Set en soit le niveau 0).
Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).
Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
appels à type_of et get_type_of sont souvent utilisés pour construire
des termes à partir de types; on ne rajoute pas non plus de
contraintes inutiles parce que type_of et get_type_of ne changent pas
le graphe de contraintes; tout ce qu'on perd est une information
utilisateur sur le type en lui-même mais puisque pretty.ml n'appelle
ni type_of ni get_type_of, ces informations sur la représentation
interne des univers restent a priori accessibles pour l'utilisateur.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Variable, et plus de trucs useless qui traînaient par ma faute (y
compris dans le noyau, la honte).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
Printing Universes est active.
Ajout de l'option "using" à la tactique non documentée "auto decomp".
Ajout de la base "extcore" pour étendre "auto decomp" avec des
principes élémentaires tels que le dépliage de "iff".
Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
details).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
les interfaces de module (bug similaire à #1302 mais pour les
définitions -- au lieu des inductifs)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9505 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Amélioration affichage des univers. Réparation de petits oublis du premier
commit. Essai d'une nouvelle stratégie : si le type d'une constante
est mentionné explicitement, la constante est monomorphe dans Type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- prise en compte du niveau à la déclaration du type comme une fonction
des sortes des conclusions des paramètres uniformes
- suppression du retypage de chaque instance de type inductif (trop coûteux)
et donc abandon de l'idée de calculer une sorte minimale même dans
des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7352 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6994 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
extensibilité aux contraintes numériques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6992 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@6244 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 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@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
| |
- reduction du noyau (variables existentielles, fonctions auxiliaires
pour inventer des noms, etc. deplacees hors de kernel/)
- changement de noms de constructeurs des constr (suppression de "Is" et
"Mut")
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
sens pour plus de partage entre chemins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
lieu de string)
Table des noms qualifiés
- Remplacement de la table de visibilité par une table qui ne cache
plus les noms de modules et sections mais seulement les noms des
constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
module A déjà existant : seuls les noms de constructions de l'ancien
A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
constantes définies à l'intérieur de sections et simplification
connexes (suppression de END-SECTION, une seule table de noms qui ne
survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
Require and co, tests de cohérence; pour être cohérent avec la non
survie des tables de noms à la sortie des section, les require à
l'intérieur d'une section eux aussi sont refaits à la fermeture de la
section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1772 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
elimination des compteurs globaux de metas et d'evars du noyau
nettoyage de safe_typing.ml (plus de flags)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
pour les noms de modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
- univers fonctionnels
- erreurs de typage maintenant sous forme d'exception,
déclarées dans Type_errors
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@24 85f007b7-540e-0410-9357-904b9bb8a0f7
|
glondu
letouzey
herbelin
soubiran
barras
aspiwack
sacerdot
filliatr
coq