aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* majGravatar coq2005-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6580 85f007b7-540e-0410-9357-904b9bb8a0f7
* This commit corrects the last commit of Hugo that broke down the "make depend"Gravatar sacerdot2005-01-12
| | | | | | | command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6578 85f007b7-540e-0410-9357-904b9bb8a0f7
* The new tutorial on (co)inductive types by Pierre Casteran.Gravatar sacerdot2005-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6577 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6575 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6573 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6571 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6569 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6567 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6565 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
* majGravatar coq2005-01-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6562 85f007b7-540e-0410-9357-904b9bb8a0f7
* [ Waiting for a keyword to control expansion during functor application ]Gravatar sacerdot2005-01-05
| | | | | | | | | 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
* majGravatar coq2005-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6559 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6557 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6556 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-03
| | | | | | printers dans ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6554 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6552 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6551 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; 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
* Réactivation d'un outil d'affichage pour le débogueur compatible avec ↵Gravatar herbelin2005-01-02
| | | | | | ocaml 3.07 et 3.08 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6549 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour permettre le chargement des printers en ocamldebug >= 3.07 : renommage ↵Gravatar herbelin2005-01-02
| | | | | | 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
* MAJGravatar herbelin2005-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6547 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
* Découpage des printers pour ne pas avoir de dépendances en la vm dans les ↵Gravatar herbelin2005-01-02
| | | | | | printers de ocamldebug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵Gravatar herbelin2005-01-02
| | | | | | dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-01-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵Gravatar herbelin2005-01-01
| | | | | | Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6541 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵Gravatar herbelin2004-12-31
| | | | | | Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de la dépendance en Tacmach pour pouvoir être appelé de ↵Gravatar herbelin2004-12-31
| | | | | | 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
* Compatibilité ancien nom de ocamldebug-coqGravatar herbelin2004-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6536 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement ocamldebug-v7 par lien symbolique ne marche pas, finalement, ↵Gravatar herbelin2004-12-31
| | | | | | création du lien par configure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6535 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement ocamldebug-v7 par ocamldebug-coq (2ème)Gravatar herbelin2004-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6534 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6531 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ↵Gravatar herbelin2004-12-30
| | | | | | 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
* majGravatar coq2004-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6528 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6527 85f007b7-540e-0410-9357-904b9bb8a0f7
* ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵Gravatar herbelin2004-12-29
| | | | | | 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
* Bug control_only_guardGravatar herbelin2004-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout printer bigintGravatar herbelin2004-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6523 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug transformation assert dans commit précédentGravatar herbelin2004-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6522 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6518 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6516 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)Gravatar herbelin2004-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout test bug 860Gravatar herbelin2004-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6513 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement du coeur d'omega (omega.ml) par la version plus générale ↵Gravatar herbelin2004-12-27
| | | | | | utilisée par romega (omega2.ml, qui, à l'occassion, disparaît sous ce nom) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise ↵Gravatar herbelin2004-12-27
| | | | | | par romega (omega2.ml, qui, l'occassion, disparat sous ce nom) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2004-12-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6509 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-23 15:57:19 +0000