| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Renommage de Rlt_not_le de Fourier_util en Rlt_not_le_frac_opp pour
éviter la confusion avec le Rlt_not_le de RIneq.
- Quelques variantes de lemmes en plus dans RIneq.
- Déplacement des énoncés de sigT dans sig (y compris la complétude)
et utilisation de la notation { l:R | }.
- Suppression hypothèse inutile de ln_exists1.
- Ajout notation ² pour Rsqr.
Au passage:
- Déplacement de dec_inh_nat_subset_has_unique_least_element
de ChoiceFacts vers Wf_nat.
- Correction de l'espace en trop dans les notations de Specif.v liées à "&".
- MAJ fichier CHANGES
Note: il reste un axiome dans Ranalysis (raison technique: Ltac ne
sait pas manipuler un terme ouvert) et dans Rtrigo.v ("sin PI/2 = 1"
non prouvé).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10710 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
en préparation du passage à des inductifs à polymorphisme de sorte
("sigT R" va devenir de type le type de R, càd Set)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
documentee).
Reste a retablir la semantique de pose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5141 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
par les fichiers nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3917 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
global
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3564 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3511 85f007b7-540e-0410-9357-904b9bb8a0f7
|