aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.ml
Commit message (Collapse)AuthorAge
...
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch bug 2313.Gravatar soubiran2010-05-05
| | | | | | | Including a module or module type into the top module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
| | | | | | Simplified in passing generation of names for the "Goal" command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12910 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplify backtrackingGravatar vgross2010-02-12
| | | | | | | As we can now jump right onto a closed segment, there is no need for complicated pattern matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing closing of segments.Gravatar vgross2010-02-12
| | | | | | You can now BackTo directly inside segments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12757 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2168 (closing a section may have as side-effect the erasureGravatar herbelin2009-11-11
| | | | | | of objects having the same name as the section). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12496 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug introduced in revision 12265.Gravatar herbelin2009-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12378 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
| | | | | | | by Context. Now Context has exactly the same semantics as Variables. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12329 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
| | | | | | | | | | only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix extract hyps to correctly discharge all hyps as described by keepGravatar msozeau2009-05-29
| | | | | | | lists. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12154 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
| | | | | | | | | | definitions and variables (may increase the vo's size a bit), which in turn fixes discharging with manual implicit args only. Fix Context to correctly handle "kept" assumptions for typeclasses, discharging a class variable when any variable bound in it is used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11765 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Synchronized subst_object with load_object (load_and_subst_objects)Gravatar herbelin2008-11-23
| | | | | | | | | | | | | | | | | | and set Declare ML Module as a regular substitutive object so that Declare ML Module is treated at the right place in the order of appearance of substitutive declarations of a required module. - Note: The full load/import mechanism for modules is not so clear: the Require part of a Require Import inside a module is set outside the module at module closing but the Import part remains inside (why not to put the "special" objects in the module too?); moreover the "substitute" and "keep" objects of a module are desynchronised at module closing (is that really harmless/necessary?). - Treatment of .cmxs targets in coq_makefile and in coqdep. - Better make clean in coq_makefile generated makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11623 85f007b7-540e-0410-9357-904b9bb8a0f7
* broke cyclic dependenciesGravatar barras2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
| | | | | | | | | setting "Set Manual Implicit Arguments" for manual-only implicits. Fix test-suite script. This removes the discharge_info argument of "dynamic" object's rebuild function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
| | | | | | | Correction au passage d'un bug de Arguments Scope Global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Prise en compte des frozen state de Coq autant que possible pourGravatar herbelin2008-05-24
| | | | | | | | | | | améliorer l'efficacité du undo. Restent les Qed et les End dont le undo peut nécessiter de rejouer un segment arbitrairement complexe (pour le undo du Qed, il faudrait typiquement que Coq se souvienne de l'entrelacement de déclarations et de tactiques). - Code mort concernant les mots-clés dans coq.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
| | | | | | | commit 10916 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
| | | | | | | | | | | | whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
| | | | | | | | | | - New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* 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
* 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
* 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
* 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
* 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
* 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
* 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
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conformité au principe du nouveau warning X de ocaml 3.09Gravatar herbelin2005-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving centralised discharge into dispatched discharge_function; required to ↵Gravatar herbelin2005-02-18
| | | | | | delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du reset des numéros d'états dans reset_initial. Plus propreGravatar coq2005-02-10
| | | | | | | pour proofgeneral. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit changement dans la gestion des nouveaux labels d'état (pour leGravatar coq2005-01-31
| | | | | | | | | backtrack en mode emacs): quand on fait un reset, on fait revenir le label courant au bon numéro (sinon d'anciens numéros toujours utilisés dans le buffer emacs deviennent obsolètes). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mémorisation numéro commande courante + reset vers ce numéro pour ↵Gravatar herbelin2005-01-14
| | | | | | mode emacs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6587 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
| | | | | | | | | | | | | | | | | * "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | 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
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 23:42:31 +0000