aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-11-12Mise en place systeme de renommage des noms de variables liees dans la ↵herbelin
bibliotheque standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4867 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJ ZArith; contraintes plus faibles pour decider la capacite a interpreter ↵herbelin
les numeraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4866 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Test de la reference principale plutot que le module dans lequel se trouve ↵herbelin
la reference pour l'interpretation des numeraux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4865 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4864 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Idtac peut prendre un argument à affichernarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12On sait jamaisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4862 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12conseille l'utilisation de la release officielle 2.2.0 de lablgtkletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4861 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12petits changements de syntaxebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12deux doigts d'extraction dans le CHANGES pour la V8letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4859 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12les modifs depuis la 7.4letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4858 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12TODOletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4857 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-12Extraction Module M devient simplement Extraction Mletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4856 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4855 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10MAJ OTHERFLAGSherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4854 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Re-suppression de is_verbose dans Print, pour coqideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4853 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10Suppression SearchNamed finalement redondant avec SearchAboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4852 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10le pb du <<.v vu comme module>> engendre maintenant une erreurletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4851 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10message informant de l'ecriture d'un fichier extraitletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4850 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10révision du traitement des axiomes non réalisésletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4849 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4848 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-10essai d'extraction sous un moduleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4847 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Quelqes renommages lies a Zorderherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4846 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Ajout quelques lemmes; noms des variables lieesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4845 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09make moins verbeux, suite (et fin?)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4844 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09factorisation de (recursive) libraryletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4843 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4842 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local defherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4841 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Traduction semantique des InHyp de clause en InHypValue si local def; ↵herbelin
simplification suite fusion eq/eqT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4840 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Mise en place traduction des tactiques apres evaluation pour permettre des ↵herbelin
changements semantiques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4839 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09'as' avant 'using' dans 'destruct'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4838 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Test Generalizeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4837 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Ajout pf_applyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4836 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09Ajout reduce_to_quantified_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4835 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-09'NewDestruct using' s'applique maintenant aussi aux types non inductifs; bug ↵herbelin
de Generalize Dependent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4834 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Code obsoleteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4833 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Fusion de tuple_constr/tuple_pattern dans operconstr/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4832 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4831 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4830 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Ajout option -impredicative-setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4829 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Suppression StronglyClassical, StronglyConstructive devient plus ↵herbelin
concretement ImpredicativeSet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4827 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Oubli BinNatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4826 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Oubli d'un Set Implicit Argumentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatif; ↵herbelin
Hurkens_set disparait de la biblio standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans mention de la possibilite d'etre impredicatifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07Biblio standard sans impredicativiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4822 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4821 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Added Instantiate ... incorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Des oublisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-06Report des definitions sorties de fast_integer pour compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4818 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 19:41:39 +0000