aboutsummaryrefslogtreecommitdiff
path: root/library/declare.ml
AgeCommit message (Collapse)Author
2008-07-24broke cyclic dependenciesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11253 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
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
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
de l'argument donné contient des métavariables (souhait #1408). Beaucoup d'infrastructure autour des constantes pour cela mais qu'on devrait pouvoir récupérer pour analyser plus finement le comportement des constantes en général : 1- Pour insérer les coercions, on utilise une transformation (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml. 2- Pour la compatibilité, on s'interdit d'insérer une coercion entre classes flexibles parce que sinon l'insertion de coercion peut prendre précédence sur la résolution des evars ce qui peut changer les comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN). 3- Pour se souvenir rapidement de la nature flexible ou rigide du symbole de tête d'une constante vis à vis de l'évaluation, on met en place une table associant à chaque constante sa constante de tête (heads.ml) 4- Comme la table des constantes de tête a besoin de connaître l'opacité des variables de section, la partie tables de declare.ml va dans un nouveau decls.ml. Au passage, simplification de coercion.ml, correction de petits bugs (l'interface de Gset.fold n'était pas assez générale; specialize cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml]; whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml]) et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml, classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
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
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
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
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
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
2007-01-10Nouvelle approche pour le discharge modulaireherbelin
- 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
2006-09-01Indentation + typonotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Standardisation nom option_app en option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-28Réorganisation de la structure interne des types de déclarations (decl_kinds)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-02Changement des named_contextgregoire
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
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-02Types inductifs parametriquesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Moving centralised discharge into dispatched discharge_function; required to ↵herbelin
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
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
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-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12option -no-hash-consing pour supprimmer le hash-consingfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6201 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-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31Export de l'information si un inductive est un record ou non (pour xml)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5622 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations ↵herbelin
utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Memorisation du type de variable (Hyp or Var)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5573 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-07Correction du bug 335 et Export/Require Export dans un modulecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-12Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵herbelin
interp et déclarations des scopes d'argument dans Declare git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4364 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Réorganisation de Impargs + mise en place d'une infrastructureherbelin
(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-19Petit netoyage dans libcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-16Petit netoyage des open's et commentairescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3448 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-11Essai de hconsing local au declarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3422 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Hash-consing dès la lib_stkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3411 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- 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
2002-11-05Intégration des modifs de la branche mowgli :herbelin
- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3031 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
les contextes de preuves git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2972 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵herbelin
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
2002-04-16Déplacement/renommage de Class.stre_max en Declare.strength_minherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2648 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-04-12Interdiction de nommer une constante comme une variable de section (plus ↵herbelin
simple que d'afficher en nom long...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2637 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras
- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-14option -dump-glob pour coqdocfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12Raffinement library_partherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2472 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-02-12Ajout library_partherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2467 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Mise en place d'une méthode directe pour indiquer le type des déclarations ↵herbelin
à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:13:06 +0000