aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-10-29*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4742 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-29Choix sous sa forme relationnelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4741 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4740 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4739 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ordre (symbolique) des Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4738 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Passage de la notations de paire dans core_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4737 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Passage des notations de type dans type_scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4736 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout notations pour les expressions dans un anneauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4735 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Simplification preuveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4734 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout de Print Visibilityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4733 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Ajout %core; MAJ niveau connecteurs logiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4732 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Affichage Assert_failure en ocaml 3.07herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4731 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Message inductive largeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Nouveaux fichiers dans Logicherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4729 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Nouveaux fichiers dans Logic; prise en compte de l'option ↵herbelin
-strongly-classical la compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4728 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Options -strongly-constructive et -strongly-classicalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4727 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Set devient predicatif par defautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4725 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4724 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Fichier offrant l'axiome du choix en presence de logique classiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4723 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28La logique sur Type inclut celle sur Setherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4722 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Retour en arriere sur d'autres renommages de variablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4721 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Retour a un nommage non standard des variables pour compatibilite; report ↵herbelin
'relation' pour compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4720 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Bug Double Inversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4719 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4718 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Nouveaux renommages; mot-cle 'exists'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4717 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-27Bug du commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4716 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4715 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Saut de ligne avant les infos non logiques de print_aboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4714 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4713 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4712 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Independance de grammar.cmo vis a vis de Searchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4711 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Conjecture declare maintenant un axiome; reorganisation VernacDefinitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4710 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4709 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-23Jprover bugfix (hopefully !)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4707 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4706 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Deplacement de iter_constr_with_full_binders dans Termopsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4705 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4704 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Ajout NArithRingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4703 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4702 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Documentation/Structurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4701 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4700 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Suppression dependance formelle en Vernacexprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4699 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Integration de SearchNamed dans SearchAboutherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4698 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22Deplacement du pr_reference du traducteur dans Ppconstrnew; integration de ↵herbelin
SearchNamed dans SearchAbout git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4697 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22reorganisation des niveaux (ex: = est a 70)barras
Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-22nouvelles priorites + Hintsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4695 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation ↵herbelin
par Pptactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4694 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Nouveaux renommages; Traduction speciale pour 'length nil'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4693 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-21Redondance de dec_eq_natherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4692 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 05:13:47 +0000