aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
...
* - 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
* HUGE COMMITGravatar sacerdot2005-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵Gravatar herbelin2005-01-02
| | | | | | printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 'Locate Library lib' quand 'lib' est aussi un moduleGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6318 85f007b7-540e-0410-9357-904b9bb8a0f7
* dead (and obsolete) code (in comments) removedGravatar sacerdot2004-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
| | | | | | | | | | | the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 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
* code mortGravatar herbelin2004-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6288 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte dans cut_ident des idents de la form _23 qui sont ↵Gravatar herbelin2004-10-12
| | | | | | officiellement autorisés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6205 85f007b7-540e-0410-9357-904b9bb8a0f7
* option -no-hash-consing pour supprimmer le hash-consingGravatar filliatr2004-10-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6201 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6198 85f007b7-540e-0410-9357-904b9bb8a0f7
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 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
* bug #780: compilation of several units in the same coqtop processGravatar barras2004-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5900 85f007b7-540e-0410-9357-904b9bb8a0f7
* correspondance des records et noms de champs de records entre un module et ↵Gravatar letouzey2004-06-25
| | | | | | sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ numéro magiqueGravatar herbelin2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de l'information si un inductive est un record ou non (pour xml)Gravatar herbelin2004-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5622 85f007b7-540e-0410-9357-904b9bb8a0f7
* The XML exportation hook for require is now active for:Gravatar sacerdot2004-03-30
| | | | | | | | | | - Require id. - Require Export id. - Require "file". - Require Export "file". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction entre declarations internes (p.ex. _subproof) et declarations ↵Gravatar herbelin2004-03-30
| | | | | | utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
* Crocret xml pour RequireGravatar herbelin2004-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Crochets pour exported les sections en xmlGravatar herbelin2004-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Memorisation du type de variable (Hyp or Var)Gravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5573 85f007b7-540e-0410-9357-904b9bb8a0f7
* preparation packages V8.0-cdromGravatar barras2004-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug de Require multipleGravatar herbelin2004-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5261 85f007b7-540e-0410-9357-904b9bb8a0f7
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement numero magique; message d'erreur en cas de mauvaise syntaxeGravatar herbelin2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reset Initial uniquement interactivementGravatar herbelin2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5113 85f007b7-540e-0410-9357-904b9bb8a0f7
* name_app accessible a tous dans NameopsGravatar herbelin2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Options -strongly-constructive et -strongly-classicalGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conjecture declare maintenant un axiome; reorganisation VernacDefinitionGravatar herbelin2003-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de iter_constr_with_full_binders dans TermopsGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle fonction cherchant tous les noms d'un suffixe donneGravatar herbelin2003-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un couple 'Conjecture/Admitted' pour déclarer un énoncé ↵Gravatar herbelin2003-10-08
| | | | | | incomplètement prouvé comme axiome git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fonctions utilesGravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵Gravatar herbelin2003-09-12
| | | | | | | | | choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵Gravatar herbelin2003-09-12
| | | | | | interp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4365 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à ↵Gravatar herbelin2003-09-12
| | | | | | 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
* errorGravatar herbelin2003-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4328 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export process_module_bindings pour traducteurGravatar herbelin2003-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4292 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4255 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage des noms de tactiques à kernel_name pour compatibilité avec les ↵Gravatar herbelin2003-06-10
| | | | | | foncteurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4116 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4115 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension renommageGravatar herbelin2003-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 20:29:28 +0000