aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* MAJGravatar herbelin2006-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8137 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'exists! x:A, PGravatar herbelin2006-02-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage Zmin.v, création Zmax.v et Zminmax.vGravatar herbelin2006-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bibliothèque String de Laurent ThéryGravatar herbelin2006-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8010 85f007b7-540e-0410-9357-904b9bb8a0f7
* Idem numbering of 'Unfold', 'simpl', ...Gravatar herbelin2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en conformité de l'ordre des occurrences de pattern avec l'affichageGravatar herbelin2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8000 85f007b7-540e-0410-9357-904b9bb8a0f7
* coq_makefileGravatar herbelin2006-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7995 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ (synonymes de Lemma; auto using)Gravatar herbelin2006-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7945 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export eassumptionGravatar herbelin2006-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7894 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extended Unicode supportGravatar herbelin2006-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomGravatar herbelin2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
| | | | | | | | - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns - TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout paramétricité du nom de la base de hint dans auto et trivialGravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur; ↵Gravatar herbelin2005-12-26
| | | | | | changements collatéraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7737 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7714 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declare Implicit TacticGravatar herbelin2005-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7365 85f007b7-540e-0410-9357-904b9bb8a0f7
* add a left and right tactic for classical logicGravatar narboux2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
* foldGravatar herbelin2005-07-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added entry constr_may_eval for tactic extensions (new syntax)Gravatar herbelin2005-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7162 85f007b7-540e-0410-9357-904b9bb8a0f7
* New environment variable COQREMOTEBROWSER to set the command used by CoqGravatar sacerdot2005-05-26
| | | | | | | | and coqide to control a remote browser. It uses the standard syntax where "%s" is the placeholder for the URL. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7077 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implemented autorewrite with ... in hyp [using ...].Gravatar sacerdot2005-05-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* possibilité d'écrire [foo| ] au lieu de [foo|idtac]Gravatar letouzey2005-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed hypotheses of Z_lt_induction (see #957)Gravatar herbelin2005-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵Gravatar herbelin2005-03-29
| | | | | | hypothesis of Zlt/Zgt_square_simpl (cg #948) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6898 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵Gravatar herbelin2005-03-07
| | | | | | statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
| | | | | | | "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
* - 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
* 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
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout 'Locate Module'Gravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6320 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6289 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des notations récursives dans l'option 'format'Gravatar herbelin2004-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6286 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵Gravatar herbelin2004-10-11
| | | | | | evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Incorrection exportation XMLGravatar herbelin2004-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement pas de liste des contributions (cela n'avait été fait que pour ↵Gravatar herbelin2004-04-17
| | | | | | la 7.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelles majsGravatar herbelin2004-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5682 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5675 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5591 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-03-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5521 85f007b7-540e-0410-9357-904b9bb8a0f7
* preparation pour release (suite)Gravatar barras2004-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5497 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-19 18:15:54 +0000