aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2007-01-02Add f_equal case for 6 arguments.msozeau
2006-10-24Ajout de la tactique 'remember'herbelin
2006-10-17Mise en forme des theoriesnotin
2006-10-05revision de la semantique de rewrite ... in <clause>. details dans la docletouzey
2006-09-22Ajout d'une valeur VList dans tacinterp pour permettre de cabler desherbelin
2006-09-21incomplete and temporary fix for PR#1222: revert accepts up to 10 argsletouzey
2006-08-28Passage à une définition de inhabited plus dans les 'standard mathématique...herbelin
2006-06-25repetition d'hypotheses dans well_founded_induction_type_2letouzey
2006-06-09Modification déf de exists! pour éviter une éta-expansion et pouvoir être...herbelin
2006-06-04Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...herbelin
2006-06-04Ajout exists! et restructuration/extension des fichiers sur laherbelin
2006-05-29Ajout d'alias pour prodT_rect et cie qui avaient été oublkÃiésherbelin
2006-05-28- Déplacement des types paramétriques prod, sum, option, identity,herbelin
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...notin
2006-03-17Modification des propriétés (svn:executable)notin
2006-03-04Titres moins envahissants pour coqdocherbelin
2006-02-27quelques raccourcis commodes + un f_equal plus efficaceletouzey
2006-02-23Ajout 'exists! x:A, P (suite)herbelin
2006-02-23Ajout 'exists! x:A, Pherbelin
2006-02-10code mortherbelin
2006-02-06Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...herbelin
2006-01-22Application de la suggestion de Nicolas Magaud (#1060)herbelin
2006-01-21Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...herbelin
2006-01-21Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Accherbelin
2006-01-19Correction associativité de IF et exists (visible à l'affichage uniquement ...herbelin
2005-12-22Contrepartie de la suppression des boites automatiques dans formatherbelin
2005-11-30changement parametres inductifs dans les theoriesmohring
2005-08-26*** empty log message ***letouzey
2005-05-19Documentationherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-03-31Added option_mapherbelin
2005-02-23quelques tactics ltacletouzey
2005-02-04Essai d'utilisation de 'where' pour les notationsherbelin
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
2005-02-03Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateursherbelin
2004-12-06Inutile de réserver les notations à base de '{ }'herbelin
2004-11-12Changement dans les boxed values .gregoire
2004-08-01Commentaires coqdocherbelin
2004-07-16Nouvelle en-têteherbelin
2004-04-06sumbool et sumor affich avec 'if' si possibleherbelin
2004-03-29Commentairesherbelin
2004-03-17Definition de la notation de la paire par un motif recursifherbelin
2004-02-28MAJ Commentairesherbelin
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
2004-01-09Commentaires en v8herbelin
2003-12-23Finalement, espacement autour du ':' pour a la fois exists, forall et funherbelin
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
2003-12-15modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesbarras
2003-12-05power associe a droitemarche