aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
Commit message (Collapse)AuthorAge
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
| | | | | | | | | maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans le kernel : Gravatar bgregoir2006-12-11
| | | | | | | | | | | | | | | | | | | | | - essai de suppression des dependances debiles. (echec) - Application des patch debian. Pour ring et field : - introduciton de la function de sign et de puissance. - Correction de certains bug. - supression de ring_replace .... Pour exact_no_check : - ajout de la tactic : vm_cast_no_check (t) qui remplace "exact_no_check (t<: type of Goal)" (cette version forcais l'evaluation du cast dans le pretypage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9319 85f007b7-540e-0410-9357-904b9bb8a0f7
* LegacyRfield was opening R_scopeGravatar barras2006-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9317 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le caractère ² fait planter make docGravatar notin2006-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en forme des theoriesGravatar notin2006-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
* separation de RealFieldGravatar barras2006-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9187 85f007b7-540e-0410-9357-904b9bb8a0f7
* commit de field + renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9179 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage sqtr_lem_1 (bug 1189)Gravatar notin2006-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵Gravatar herbelin2006-07-11
| | | | | | Rfun_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %F) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9042 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ↵Gravatar herbelin2006-05-22
| | | | | | bas, i.e. Set; renommage canonique Rmax_comm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8838 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ suite placement automatiquement de Rlist au niveau prédicatif le plus ↵Gravatar herbelin2006-05-22
| | | | | | bas, i.e. Set; renommage canonique Rmax_comm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* New unification can solve the problem without eta-expansion, Gravatar msozeau2006-04-10
| | | | | | | but is bugguy with it. Temporary fix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8691 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nommage explicite de certains "intro" pour préserver la compatibilitéGravatar herbelin2006-03-28
| | | | | | | | 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
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
* Détection d'un Fold incorrect suite à correction bug #986Gravatar herbelin2005-07-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7219 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing translating a 'O' into a '0' (again)Gravatar herbelin2005-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6897 85f007b7-540e-0410-9357-904b9bb8a0f7
* compatibility with POWERPCGravatar gregoire2004-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout decimal_exp pour interpreter les notations decimalesGravatar mohring2004-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de Rsyntax en v8Gravatar herbelin2004-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5197 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugs avec Pose et AssertGravatar barras2004-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
* changement de pose en set (pose n'etait pas utilise avec la semantiqueGravatar barras2003-12-24
| | | | | | | | 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
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
* power associe a droiteGravatar marche2003-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ratage standardisation Rge_monotony en Rmult_ge_compat_rGravatar herbelin2003-12-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5047 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ↵Gravatar herbelin2003-11-29
| | | | | | par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation locale pour RpowerGravatar herbelin2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout lemmes, simplification preuve de SeqPropGravatar herbelin2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation du total_order non constructifGravatar herbelin2003-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Protection contre les renommages; redondancesGravatar herbelin2003-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration compatibilite 7.4 pour le Hint Unfold RgtGravatar herbelin2003-11-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleure solution pour la compatibiliteGravatar herbelin2003-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4921 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ INZGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration preference Rge a Rle pour compatibilite...Gravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4769 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restauration preference Rge a Rle pour compatibilite...; petit nettoyageGravatar herbelin2003-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4768 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵Gravatar herbelin2003-10-30
| | | | | | associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
* reorganisation des niveaux (ex: = est a 70)Gravatar barras2003-10-22
| | | | | | | 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
* R passe dans Set !Gravatar herbelin2003-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4677 85f007b7-540e-0410-9357-904b9bb8a0f7
* 20 est uniquement associatif a gaucheGravatar herbelin2003-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4672 85f007b7-540e-0410-9357-904b9bb8a0f7
* lettac -> setGravatar barras2003-10-16
| | | | | | | suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pour eviter des regles redondantes en v7Gravatar herbelin2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4647 85f007b7-540e-0410-9357-904b9bb8a0f7
* FTC_P2 maintenant dans RIneqGravatar herbelin2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4646 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de quelques lemmes clesGravatar herbelin2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4645 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage = au lieu de == en v7Gravatar herbelin2003-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4642 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-27 00:19:40 +0000