aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-01-25majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6639 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-25Ajout dependance LIBCOQRUN pour coqide et coq-interfaceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6638 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-25sed ne connait pas '+' sur macosxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6636 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-24majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6634 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-23majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6632 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-22majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6629 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6625 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Modification cible doc/coq.tex pour tenir des .mli qui n'existent pas ↵herbelin
toujours (mais nécessite une archive intègre sans .mli non déclarés) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6624 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6623 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Pour cible make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6620 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-21Compatibilité ocamlweb pour cible docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-20majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6610 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-19majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6608 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-18majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6606 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-18Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of thesacerdot
term to be replaced in the term that is the morphism was done too early (before computing the "morphism family" parameters). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6605 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6603 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6602 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-17Bug fixed (reported by Roland): the setoire_rewrite in tactic did not worksacerdot
in the followin case: H : t < c1 H0: c1 < c2 ============= t' setoid_rewrite H0 in H Explanation: the tactic made a cut with H0: c1 < c2 =============== t < c2 and then did setoid_rewrite <- H0 in H. If c2 occurs in t, then the tactic may fail (due to wrong variance). The simple fix consists in changing "t < c2" to "let H := c2 in t{H/c2} < c2" and then perform an intro before proceeding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6601 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-171. added code to handle the inclusion of inductive types and constructors insacerdot
parameters. 2. however, the code is still not working if the parameters are referenced later on in the module signature. To fix this the representation of terms must be changed to unify references to constants, inductive types and constructors. 3. thus the code above is prefixed by an error that suggest to the user how to avoid the problem right now. Note: the above code has not been commented out to keep it in synch with the other changes in the kernel. However, it is dead code for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6600 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-16majcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6598 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 04:22:03 +0000