aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2006-12-03Remplacement de la dépendance de G_vernac en G_constr (sourceherbelin
d'incohérences dans les dépendances en l'absence de g_constr.mli) par une dépendance en Topconstr git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9409 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Correction boucle du parseur en cas de caractÃère non unicodeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9394 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-20Suppression du type 'tac dans les abstract_argument_type: devenu inutile herbelin
suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des wit_tactic en types créés dynamiquement (révisions 8917 et 8926). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9393 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-17The emacs-U option now does not output *any* char above 250.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9384 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-11Fichiers obsolètesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9367 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-11-02gestion speciale du niveau 5 des ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9333 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31syntaxe du let in encorebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9325 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-31assouplissement de la syntaxe du let de ltac: t1 ; let in autorisebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9324 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-30fixed field_simplify + changed precedence of let and fun in ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-29Exports manquants dans ringbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9315 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-29Compatibilité du polymorphisme de constantes avec les sections.herbelin
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
2006-10-28Extension du polymorphisme de sorte au cas des définitions dans Type.herbelin
(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Documentation de "Set Printing Universes", "Print Universes" (anciennementherbelin
"Dump Universes"), "Universe inconsistency", et description brève des univers algébriques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9306 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-28Ajout option Set Printing Universes et amélioration affichage des universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9304 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Extension de la primitive ltac fresh pour qu'elle accepte une liste deherbelin
noms et de chaînes qu'elle va concaténer pour créer un nom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9267 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Hack peu élégant pour permettre de parser des listes avec séparateurs dans herbelin
TACTIC EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9265 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-19coqide: affichage des sous-buts et hypothèses et métas comme types deherbelin
telle sorte que les coercions vers sortclass ne soient pas affichées (comme dans coqtop) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-16affichage des ... dans les scriptsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-09Notations:herbelin
- prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-03le parsing du LETIN ne suivait pas la DTD (bug #1237)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9200 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-28Suppression des lignes vides dans l'affichage des scriptsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9186 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-23Déplacement surround dans util.ml et parenthésage des déclarationsherbelin
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
2006-09-20Declarative Proof Language: main commitcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-15Compatibilité hyp=var dans Tactic Notation + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9147 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
(+ uniformisation position notation dans les blocs inductifs et récursifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22making otags working jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-12Correction incohérence parsing de %delim dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9043 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Utilisation du mot-clé lazymatch pour le match paresseux (à défaut ↵herbelin
d'avoir trouver mieux) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9037 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, ↵herbelin
renommage en 'Set/Unset Ltac Debug' en prévision documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9020 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, ↵herbelin
renommage en 'Set/Unset Ltac Debug' en prévision documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9017 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Nettoyage code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9016 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05Correction typo + ajout Arabic Supplementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9015 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ↵herbelin
pattern pose problème pour les notations ajoutées à ce niveau; qu'à cela ne tienne, l'associativité du niveau 100 pour pattern n'est pas importante : on le rend RIGHTA git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9008 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Mise à jour (avec retard) des niveaux de la table default_pattern_levelsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8996 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT ↵herbelin
EXTEND et TACTIC EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8982 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suppresion redondance interp_entry_name entre Q_util et Argextendherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8976 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Added {measure x f} as a valid recursion order.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-10Bug is_numberherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8947 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Plus de Declare Module sans vrai type expliciteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8929 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵notin
(fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Factorisation utilisation environnement dans make_pr_tacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8922 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-07Correction trou de subject-reduction de create_arg dans genarg.mliherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour ↵herbelin
permettre de passer les occurrences en paramètre dans ltac, par exemple à pattern git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8878 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29The "clean integration of subtac" patch.msozeau
Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Changement de précédence de l'argument du by de assert; ↵herbelin
conséquences sur les .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8853 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-23Nouvelle implantation du polymorphisme de sorte pour les familles inductivesherbelin
- 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 05:12:54 +0000