aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* majGravatar coq2005-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7032 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affinements suite à extension Tactic Notation aux tacticiellesGravatar herbelin2005-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7030 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
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles + erreur typage TacAlias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7028 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7026 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7024 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Globalisation des Tactic NotationGravatar herbelin2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7019 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7016 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7014 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7012 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7010 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7008 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7006 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
* 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@7004 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7002 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7000 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6997 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6995 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage graphe universGravatar herbelin2005-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code v7 obsoleteGravatar herbelin2005-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6993 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ commentaires et inversion du sens du graphe de contraintes pour ↵Gravatar herbelin2005-05-05
| | | | | | extensibilité aux contraintes numériques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6992 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6990 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Open Scope non Local malencontreuxGravatar herbelin2005-05-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6987 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement, préservation de la compatibilité pour Z_lt_induction et ajout ↵Gravatar herbelin2005-05-02
| | | | | | plutôt de nouveaux énoncés git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lemme de passage de l'autre côté d'une égalitéGravatar herbelin2005-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation Z_scopeGravatar herbelin2005-05-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6982 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-05-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6980 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6978 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection against saving a proof with still non-instantiated evars (cf bug ↵Gravatar herbelin2005-04-29
| | | | | | #901) (continued!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection against saving a proof with still non-instantiated evars (cf bug ↵Gravatar herbelin2005-04-29
| | | | | | #901) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6974 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved order of interpretation of atomic tactics (cf bug #952)Gravatar herbelin2005-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in prepare_predicate_from_tycon; improved error message when no ↵Gravatar herbelin2005-04-29
| | | | | | clauses and no empty inductive type found; (expected) improvement in the shifting test (match_current) on non inductive type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6969 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6967 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6965 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6963 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
* majGravatar coq2005-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6960 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6958 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6956 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6954 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar coq2005-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6952 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 22:20:02 +0000