aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-11-09make moins verbeux, suite (et fin?)letouzey
2003-11-09factorisation de (recursive) libraryletouzey
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local def; simplif...herbelin
2003-11-09Mise en place traduction des tactiques apres evaluation pour permettre des ch...herbelin
2003-11-09'as' avant 'using' dans 'destruct'herbelin
2003-11-09Test Generalizeherbelin
2003-11-09Ajout pf_applyherbelin
2003-11-09Ajout reduce_to_quantified_refherbelin
2003-11-09'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ...herbelin
2003-11-08Code obsoleteherbelin
2003-11-08Fusion de tuple_constr/tuple_pattern dans operconstr/patternherbelin
2003-11-08MAJherbelin
2003-11-08Nettoyageherbelin
2003-11-08Ajout option -impredicative-setherbelin
2003-11-08Suppression StronglyClassical, StronglyConstructive devient plus concretement...herbelin
2003-11-08majfilliatr
2003-11-07Oubli BinNatherbelin
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatif; Hurkens_s...herbelin
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatifherbelin
2003-11-07Biblio standard sans impredicativiteherbelin
2003-11-07majfilliatr
2003-11-06Added Instantiate ... incorbinea
2003-11-06Des oublisherbelin
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
2003-11-06majfilliatr
2003-11-05Notationsherbelin
2003-11-05Interpretation des entiers dans N (ex-entier), maj du module des positiveherbelin
2003-11-05Oubliherbelin
2003-11-05MAJherbelin
2003-11-052 espaces en tropherbelin
2003-11-05MAJherbelin
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Ajout répertoire NArith pour l'arithmétique binaire sur les nombres positif...herbelin
2003-11-05Preuve de l'incoherence de {A}+{~A} avec Set impredicatifherbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-05Redondancesherbelin
2003-11-05Modules obsoletes de ZArith en v8herbelin
2003-11-05Nouvelle vague de renommageherbelin
2003-11-05Déport des lemmes de Omega de ZArith vers OmegaLemmasherbelin
2003-11-05Ajout NArith et restructuration ZArithherbelin
2003-11-05Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de...herbelin
2003-11-05MAJherbelin
2003-11-05Renommage canonique d'un lemme redondantherbelin
2003-11-05Branchement de Show Script sur l'afficheur structureherbelin
2003-11-05Amelioration de l'afficheur de script structureherbelin
2003-11-05majfilliatr
2003-11-04En v8, une notation, c'est 2 regles et un niveauherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-24 18:50:17 +0000