| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
castées si aussi suivies de leur type (p.ex. dans les hypothèses de but),
afin d'éviter des configurations non réinterprétables comme x:nat:nat.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9164 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9151 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9130 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8867 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
Correction d'un bug dans add_glob (list_chop), avec ajout des list_drop_prefix dans lib/util.ml et de drop_dirpath_prefix dans library/libnames.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8768 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
ce patch dispense d'ecrire le { struct .. }
En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind,
l'index de l'argument inductif devient un int option au lieu d'un int.
Les deux cas possibles:
- Some n : les situations autorisées auparavant, a savoir {struct}
explicite, ou bien un seul argument au total
- None : le cas nouveau, qui redonne un entier lors du passage de
rawconstr à constr si l'on trouve effectivement un unique argument
ayant un type inductif, et une erreur sinon.
Pour l'instant, on cherche l'inductif dans le type de manière
syntaxique, mais il est jouable de rajouter un poil de reduction
(au moins delta).
Dans le détail, voici les coins que ce patch influence:
- parsing/g_xml.ml4: continue pour l'instant a attendre un index
explicite via un element xml "recIndex"
- contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà
un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par
contre, dans le détail, le code pour un CFix utilise l'index de
recurrence pour recouper au besoin le type du fixpoint en deux.
Est-ce que je me gourre en supposant que si l'on a besoin de couper
ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de
l'impression d'un constr, et donc que l'index aura été correctement
résolu ?
- contrib/subtac/subtac_command.ml:
- contrib/funind/indfun.ml:
dans les deux cas, j'ai fait le service minimum, le struct reste
obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas
dur à adapter pour ceux qui comprennent ces parties.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8672 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8002 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
changé entre les version 3.08.4 et 3.09.0 (influe notamment sur l'ordre
d'application des Hints de auto)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7925 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7907 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
fixes s'affichent correctement
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5351 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5342 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
dans le module de leur définition.
Error_in_file dans Util et étendu avec possibilité de noms de modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5328 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5164 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4997 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4625 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4398 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4251 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3970 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
conversion pour permettre a Coq IDE d'interrompre Coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3871 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3320 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3289 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3136 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 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@2630 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2499 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2444 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2410 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@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2125 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@1737 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1550 85f007b7-540e-0410-9357-904b9bb8a0f7
|
herbelin
corbinea
notin
letouzey
barras
filliatr
coq