aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Collapse)Author
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
decidability of the usual equality Major changes: * andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v * added 2 files: * toplevel/ind_tables.ml* : tables where the boolean eqs and the decidability proofs are stored * toplevel/auto_ind_decl.ml* : code of the schemes that are automatically generated from inductives types (currently boolean eq & decidability ) * improvement of injection: if the decidability have been correctly computed, injection can now break the equalities over dependant pair How to use: Set Equality Scheme. to set the automatic generation of the equality when you create a new inductive type Scheme Equality for I. tries to create the equality for the already declared type I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-03Révision de theories/Logic concernant les axiomes de descriptions.herbelin
Mise à jour du tableau des axiomes dans la FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
Printing Universes est active. Ajout de l'option "using" à la tactique non documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto decomp" avec des principes élémentaires tels que le dépliage de "iff". Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Move Program tactics into a proper theories/ directory as they are general ↵msozeau
purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
cie (cf message coq-club 21/6/07). De plus, left/right inleft/inright, eux aussi dans Set/Type, y étaient déjà donc l'argument d'être dans Type n'est pas recevable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9906 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
Added a tactic "now" which is nonrecursive but generalizes "trivial". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9884 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-05Gestion espaces dans notation _ = _ :> _herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9876 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-28Déplacement des opérations sur bool dans l'état initialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9803 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-02Added back the tactics [apply -> ident], etc. to Tactics.v afteremakarov
committing the extension of the general sequence operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9743 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-01Removed the definition of extensions of apply to equivalencesemakarov
(apply -> H, etc.), which prevented Coq compilation. These tactics require an extension of syntax: t1; [t2 | .. ], which has to be submitted first. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9739 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-30Added new tactics for applying equivalences (iff) to Tactics.v:emakarov
"apply -> t", "apply <- t", "apply -> t in H" and "apply <- t in H" . Also added the tactic false_hyp based on absurd_hyp. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9737 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-26stupid me: ?f two times in a patternletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9731 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-02Add f_equal case for 6 arguments.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9469 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-24Ajout de la tactique 'remember'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9268 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-22Ajout d'une valeur VList dans tacinterp pour permettre de cabler desherbelin
Tactic Notation acceptant des listes en entrée avec application à la définition de revert dans Tactics.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9159 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-09-21incomplete and temporary fix for PR#1222: revert accepts up to 10 argsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9156 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-28Passage à une définition de inhabited plus dans les 'standard ↵herbelin
mathématiques'; ajout preuve que tous les 'epsilon i P' sont égaux si P habité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9093 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-25repetition d'hypotheses dans well_founded_induction_type_2letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8988 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Modification déf de exists! pour éviter une éta-expansion et pouvoir ↵herbelin
être filtré facilement par 'ex (unique ?P)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8936 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict ↵herbelin
with FSets git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8894 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
description et le choix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8892 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-29Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8872 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
sig, sig2, sumor, list et vector dans Type - Branchement de prodT/listT vers les nouveaux prod/list - Abandon sigS/sigS2 au profit de sigT et du nouveau sigT2 - Changements en conséquence dans les théories (notamment Field_Tactic), ainsi que dans les modules ML Coqlib/Equality/Hipattern/Field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8866 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-04Titres moins envahissants pour coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8121 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-27quelques raccourcis commodes + un f_equal plus efficaceletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8100 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-23Ajout 'exists! x:A, P (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8086 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-10code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8022 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-02-06Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et ↵herbelin
Russell O'Connor (redondance Acc_iter et Fix_F) + uniformisation indentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-22Application de la suggestion de Nicolas Magaud (#1060)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7917 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind ↵herbelin
est incompatible avec la préservation du type de Acc_intro (par uniformité de notations, x est finalement préféré) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7912 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-21Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Accherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7905 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-19Correction associativité de IF et exists (visible à l'affichage uniquement ↵herbelin
à cause du traitement spécial du niveau binder_constr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7892 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-22Contrepartie de la suppression des boites automatiques dans formatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7703 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-11-30changement parametres inductifs dans les theoriesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7630 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-08-26*** empty log message ***letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7322 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-05-19Documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7042 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-03-31Added option_mapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6903 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-23quelques tactics ltacletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6773 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Essai d'utilisation de 'where' pour les notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6675 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6670 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6666 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Inutile de réserver les notations à base de '{ }'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6410 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 23:10:42 +0000