aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-01-15majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6595 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6592 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6591 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Ajout de la syntaxe du reset label: "BackTo n".coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6590 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Affichage numéro de l'état de la commande courante pour mode emacsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6588 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Ajout mémorisation numéro commande courante + reset vers ce numéro pour ↵herbelin
mode emacs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6587 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Code redondant (cf Printer)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6586 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-13majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6584 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-13Amélioration message Locateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6583 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-12majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6580 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-12This commit corrects the last commit of Hugo that broke down the "make depend"sacerdot
command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6578 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-12The new tutorial on (co)inductive types by Pierre Casteran.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6577 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-11majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6575 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-10majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6573 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-09majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6571 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-08majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6569 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-07majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6567 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-06majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6565 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
* "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
2005-01-05majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6562 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-05[ Waiting for a keyword to control expansion during functor application ]sacerdot
When F(X: T) := B is applied to M, M.t in B{M/X} is now delta-expanded only if T.t is an axiom or a parameter. This seems to be the expected behaviour at least for orsay/FSets. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6561 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-04majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6559 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6557 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6556 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03HUGE COMMITsacerdot
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
2005-01-03Renommage 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@6554 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6552 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6551 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de ↵herbelin
printers dans ocamldebug; partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6550 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Réactivation d'un outil d'affichage pour le débogueur compatible avec ↵herbelin
ocaml 3.07 et 3.08 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6549 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage ↵herbelin
symbols.cmo en notation.cmo; nouveau redexpr.cmo; nouvelle cible dev/printers.cma pour ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6548 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6547 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
2005-01-02Découpage des printers pour ne pas avoir de dépendances en la vm dans les ↵herbelin
printers de ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6545 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵herbelin
dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-01majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6542 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-01Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵herbelin
Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6541 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6539 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵herbelin
Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6538 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Suppression de la dépendance en Tacmach pour pouvoir être appelé de ↵herbelin
top_printers sans tirer Tacred et les fichiers C de la machine virtuelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6537 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Compatibilité ancien nom de ocamldebug-coqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6536 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Remplacement ocamldebug-v7 par lien symbolique ne marche pas, finalement, ↵herbelin
création du lien par configure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6535 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-31Remplacement ocamldebug-v7 par ocamldebug-coq (2ème)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6534 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-30majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6531 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-30Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ↵herbelin
réduit aussi les types du contexte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6530 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6528 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6527 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵herbelin
convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 11:00:15 +0000