aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
AgeCommit message (Collapse)Author
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
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
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Amélioration affichage coercions vers Funclassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5799 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Heuristique pour traduire if-then-else quand le re-typage echoueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5616 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵herbelin
sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fix (2e)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5478 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de facto des fixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5477 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-14correction bug de choix de noms courts avec Suresnes/BDDbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5476 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-08correction de bugs des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-05modif des fixpoints pour que si on donne une notation au produit, les pts ↵barras
fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-26Keep structure information for Fixpoint declaration and Fix termsbertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-18- fixed the Assert_failure error in kernel/modopsbarras
- 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
2004-02-18Bug coercions imbriquees + suppression des coercions avant filtrage sur ↵herbelin
notations pour respecter le cpmt v7 et la symtrie avec le parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5357 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Correction bug affichage en presence de '{ _ }'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5323 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A*{B}+{C}" en présence d'une notation "_ * { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-03Relachement condition pour afficher @ en cas d'explicitation d'implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5285 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-29Ajout option raw_print (Set Printing All) pour desactiver toute ↵herbelin
fonctionnalite de haut niveau de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5269 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-27Bug activation erronée du traducteur en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5257 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-26reparation de qqs bugs du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-21Traduction PolyList/List dans la qualificationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-19Substitution dans REvar et PEvar plutot que encodage via noeud application ↵herbelin
pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15'Eval' protege dans Ppconstrnew; eval n'a pas le meme besoinherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5098 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Renommages discrets dans RIneq et Znumtheoryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5017 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Suite commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5011 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-27Qualification des noms utilisateurs en cas de collision avec un nom nouveauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5009 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-26Traduction de @; simplification traduction des identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5001 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25modif lexer: ident peut commencer par _barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-21ajout Pnat et Pcompare_antisymherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4967 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-19Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵herbelin
dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18reparation bug moins unaire (erreur de PP)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Mise en place systeme de qualification des noms renommes; Renommages dans ↵herbelin
Ring; Nouvelle redondance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4939 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Conflit renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4913 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Oublis dans les rennomagesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4910 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-14Suppression renommages dans Peanoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4900 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-13moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵barras
Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Nouvelle et derniere vague de renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4870 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Quelqes renommages lies a Zorderherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4846 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-05Nouvelle vague de renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4804 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-01Extensibilite de la grammaires des patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4765 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Nouveaux renommages; mot-cle 'exists'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4717 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Nouveaux renommages; Traduction speciale pour 'length nil'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4693 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-17Re-desactivation de l'affichage des projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4668 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16print_projections a true juste pour le bench nocturneherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4660 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-16Debranchement de l'affichage systematique des projections avec la notation ↵herbelin
pointee; soumis maintenant a l'activation de l'option 'Set Printing Projections' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4649 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-15Gestion encore plus affinee des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4641 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Gestion affinee des implicitesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4637 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-14Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4636 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-10changement nouvelle syntaxe (pt fixes)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-30Les notations hors scope s'empilent maintenant comme des scopes neherbelin
contenant qu'une notation + renommage dans Reals git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4505 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 07:53:19 +0000