aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
AgeCommit message (Collapse)Author
2006-03-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8137 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Ajout 'exists! x:A, Pherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-12Nettoyage Zmin.v, création Zmax.v et Zminmax.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8032 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-08Ajout bibliothèque String de Laurent Théryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8010 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Idem numbering of 'Unfold', 'simpl', ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8004 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07Mise en conformité de l'ordre des occurrences de pattern avec l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8001 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8000 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06coq_makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7995 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-29MAJ (synonymes de Lemma; auto using)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7945 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Export eassumptionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7894 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Extended Unicode supportherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7893 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nomherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7879 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-16- Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesherbelin
- 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
2006-01-11Ajout paramétricité du nom de la base de hint dans auto et trivialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7836 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7812 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur; ↵herbelin
changements collatéraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7737 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-23*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7714 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7685 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-09-09Declare Implicit Tacticherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7365 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15add a left and right tactic for classical logicnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7234 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-07-15foldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7231 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-06-22Added entry constr_may_eval for tactic extensions (new syntax)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7162 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-26New environment variable COQREMOTEBROWSER to set the command used by Coqsacerdot
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
2005-05-20New command: "Print Ltac qualid" to print user defined tactics.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-18Implemented autorewrite with ... in hyp [using ...].sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7034 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵herbelin
aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-09possibilité d'écrire [foo| ] au lieu de [foo|idtac]letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7005 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-26Fixed hypotheses of Z_lt_induction (see #957)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6962 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-29Missing translating a 'O' into a '0' (again - cf bug #947); removed useless ↵herbelin
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
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵herbelin
statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Ajout Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-06Nettoyage et documentation de Libraryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 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-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-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
2004-12-27Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Ajout 'Locate Module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6320 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-09MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6289 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-08Prise en compte des notations récursives dans l'option 'format'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6286 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵herbelin
evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17Incorrection exportation XMLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5687 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17Finalement pas de liste des contributions (cela n'avait été fait que pour ↵herbelin
la 7.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5686 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-16Nouvelles majsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5682 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5675 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5591 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5521 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-15preparation pour release (suite)barras
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.25.1) at 2026-08-13 01:14:31 +0000