aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* Amélioration du message d'erreur dans end_module, end_module_type et ↵Gravatar notin2007-10-29
| | | | | | close_section. On affiche maintenant le nom du dernier module/section ouvert git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de plusieurs bugs de l'export XML (utilisation d'un type deGravatar herbelin2007-06-21
| | | | | | | | | | | constante par defaut pour les nouveaux types plutot qu'echouer; avertissement plutot qu'echec en cas de foncteur; nommage systematique des LetIn -- p.ex. functional induction engendre des LetIn non nommes --; branchement de la fonction de normalisation de tete evitant CProp sur Closure au lieu de Tacred afin de garantir la f.n. de tete) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9902 85f007b7-540e-0410-9357-904b9bb8a0f7
* Par compatibilité, les implicites terminaux sont maximaux aussi quandGravatar herbelin2007-05-22
| | | | | | | | inférés automatiquement (pas seulement si donnés manuellement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug calcul des implicites en présence d'evars dans les typesGravatar herbelin2007-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9827 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
| | | | | | | | | | | | | discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - correction du mode strict qui n'était pas si strict, - option "Set Strong Strict Implicit" pour activer le mode strictement strict (désactivé par défaut pour raison de compatibilité), - option "Set Reversible Pattern Implicit" pour activer les implicites inférables par unification-pattern (désactivé par défaut par compatibilité), - option "Unset Printing Implicit Defensive" pour désactiver l'affichage des implicites n'ayant pas été décelés stricts, - option "Set Maximal Implicit Insertion" pour que les applications soient saturées en implicites si possible, - une optimisation du mode non strict pour que l'algo de recherche des implicites renonce à calculer les occurrences non strictes qui pourraient avoir à être affichées dans le mode défensif, avec pour conséquence que le mode défensif, pour celui qui le veut, devient a priori encore plus verbeux, ex: Set Implicit Arguments. Definition id x : nat := x. Parameter f : forall n, id n = id n -> Prop. Check (f (refl_equal O)). (* Affichait: "f (refl_equal 0)" mais affiche maintenant "f (n:=0) (refl_equal 0)" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
| | | | | | | | | | Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* (PR#1529)Gravatar soubiran2007-04-25
| | | | | | | | Now the warning will be printed when the flag verbose is on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une passe sur les warnings (ajout Options.warn déclenchée par ↵Gravatar herbelin2007-02-24
| | | | | | | | | compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles + messages divers). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1364 (les variables de section sont repérées parGravatar herbelin2007-02-07
| | | | | | | | | interp_var : ne pas les repérer à nouveau comme objets globaux, puisqu'elles ont pu être effacées dans un contexte local de but). (report revision 9611 de la branche 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9616 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1333 (test non récursivité des dépendances en d'autresGravatar herbelin2007-01-24
| | | | | | | | "library" lors de la construction d'une "library" -- i.e. d'un .vo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge with Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
| | | | | | | | - Fix previous merge (semantic/type conflict in code added minutes before my commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
| | | | | | | discharge_function des implicites au cas des scopes d'arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning backtracking code, optimized "Backtrack n x y" when n isGravatar courtieu2006-12-28
| | | | | | current state. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1041 (double cause : non évitement des noms existants enGravatar herbelin2006-12-12
| | | | | | | | | | cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml) + test régression bug #1041 + allègement syntaxe tactique evar + essai de ne pas faire dépendre les evars des variables anonymes afin de résoudre le bug #932 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9433 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)Gravatar herbelin2006-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement du magic numberGravatar notin2006-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (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
* Ajout combinateurs option_fold_left et name_fold_mapGravatar herbelin2006-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + svnpropGravatar notin2006-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + typoGravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un peu de delta-réduction...Gravatar herbelin2006-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1170: les options synchronisées déclarées dans une ↵Gravatar notin2006-07-27
| | | | | | section ne survivent plus à la fin de la section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9060 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nombre magique pour la 8.1betaGravatar herbelin2006-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #990 (LoadPath et option -R de coqideGravatar notin2006-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de add_glob (support des modules dans Coqdoc)Gravatar notin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification role de library_part : renommage en remove_section_partGravatar herbelin2006-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - 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
* r8931@thot: notin | 2006-04-28 16:19:38 +0200Gravatar notin2006-04-28
| | | | | | | | 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
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout chop_dirpathGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8745 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement anomaly en failwith dans out_name pour utilisation par map_succeedGravatar herbelin2006-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
| | | | | | | | | | | foncteurs sont données un par un ce qui permet de faire les load_objects correspondants au bon moment (càd juste après l'ajout des déclarations logiques et avant l'ajout du paramètre suivant). Ceci clôt le bug #1118 et corrige des erreurs de localisation introduite par le commit précédent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
| | | | | | | | | | | | | | | | | | | | | à la déclaration des paramètres de foncteurs (problème de synchronisation révélé par bug #1118, apparu suite à l'appel de lookup_mind par load_struct, suite au passage à un discharge local) Les objets non logiques sont maintenant chargés après car ils peuvent dépendre d'objets logiques. Et comme les objets non logiques (p.ex. l'import récursif de modules dans la nametab) sont nécessaires au typage de l'éventuelle contrainte de module, on reporte la gestion de la contrainte au moment du end_module (on aurait peut-être pu faire plus fin et extraire dans do_module la partie purement module, mais après tout le report de la contrainte de type dans le end_module ne semble pas génante). À la date d'aujourd'hui, le bug #1118 reste toutefois ouvert avec les définitions de module non interactives. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout array_fold_map', list_fold_map' et list_remove_firstGravatar herbelin2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8672 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification des propriétés (svn:executable)Gravatar notin2006-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout syntaxe concrète Proposition, synonyme de LemmaGravatar herbelin2006-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7944 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout syntaxe concrète Property/Corollary, synonymes de LemmaGravatar herbelin2006-01-28
| | | | | | | | | - Ajout syntaxe concrète Example, synonyme de Definition - Réorganisation de la structure interne des types de déclarations (decl_kinds) - Notamment, ajout de noms pour les déclarations interne (Scheme, Fixpoint...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7940 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2006-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7899 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de réparation du bug #1025: it seems like that a casted module ↵Gravatar herbelin2005-12-24
| | | | | | should only rely on the contents of its signature (i.e. with removal of the keep and special objects), doesn't it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vérification qu'un module est ouvert avant d'insérer une déclaration ↵Gravatar herbelin2005-12-23
| | | | | | nommée (peut arriver en mode -batch sans option -top) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement des named_contextGravatar gregoire2005-12-02
| | | | | | | | 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
* Fonctionnalisation du cache 'compunit' pour réparer correctement le bug ↵Gravatar herbelin2005-11-26
| | | | | | #1030 (car add_frozen_state dans cache_require du commit précédent se faisait avant le add_leaf du require et cassait l'ordonnancement de la lib_stk pour le reset) + nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7615 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 13:34:21 +0000