aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-11-10Re-suppression de is_verbose dans Print, pour coqideherbelin
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
2003-11-10révision du traitement des axiomes non réalisésletouzey
2003-11-10majfilliatr
2003-11-10essai d'extraction sous un moduleletouzey
2003-11-09Quelqes renommages lies a Zorderherbelin
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-12 19:45:12 +0000