aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Collapse)Author
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
2004-08-01Commentaires coqdocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6004 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-06sumbool et sumor affich avec 'if' si possibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5642 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5597 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-17Definition de la notation de la paire par un motif recursifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5518 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28MAJ Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5397 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A*{B}+{C}" en présence d'une notation "_ * { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09Commentaires en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5189 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Finalement, espacement autour du ':' pour a la fois exists, forall et funherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5135 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5125 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-05power associe a droitemarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:53:42 +0000