aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
| | | | | | | | | | | | | | the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1679 (congruence) et ajout test-suiteGravatar corbinea2007-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update before joining all signatures into one.Gravatar emakarov2007-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7
* - renaming Qle_shift_recip_r into Qle_shift_inv_r, etcGravatar roconnor2007-09-07
| | | | | | | | | | | | - Adding Qlt_shift_div_l, etc - Adding Qabs_Qmult : forall a b, Qabs (a*b) == (Qabs a)*(Qabs b). - Adding Qle_Qabs : forall a, a <= Qabs a. - Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs. It is already defined elsewhere (in it's proper place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7
* errors in recdef.ml4:Gravatar bertot2007-09-06
| | | | | | | | a few errors of parentheses around fun x -> ... constructs, a use of tclTHEN was left over from bug tracking modifications, it was badly parenthesized. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10117 85f007b7-540e-0410-9357-904b9bb8a0f7
* this should fix a problem described in a message by Dufourd on July 30th, 2007Gravatar bertot2007-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10116 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
| | | | | | | evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Itération sur les sous-termes dans la vérification de la condition de gardeGravatar herbelin2007-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10114 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed iconsGravatar barras2007-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10113 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed iconsGravatar barras2007-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'un nouvel algorithme plus raffiné pour prendre en compte lesGravatar herbelin2007-09-04
| | | | | | | | | | | alias de variables dans la fonction d'inversion des instance (real_clean): - détection des cas d'inversions distinctes incompatibles - nouvelle heuristique lorsque plusieurs inversions distinctes mais compatibles existent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10111 85f007b7-540e-0410-9357-904b9bb8a0f7
* A word on the measure and wf modifiersGravatar msozeau2007-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite commit 10103 (expansion des défs locales triviales dans l'étapeGravatar herbelin2007-09-01
| | | | | | | | de "projection" lors de l'instanciation d'une evar -- fonction "real_clean") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10109 85f007b7-540e-0410-9357-904b9bb8a0f7
* fin de la correction de FunctionGravatar jforest2007-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10108 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction bug d'efficacite dans FunctionGravatar jforest2007-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des paramètres Whelp et ajouts d'options Set Whelp ServerGravatar herbelin2007-08-30
| | | | | | | | | et Set Whelp Getter pour changer le nom des serveurs (report 10105 de la 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli dans commit 10102...Gravatar herbelin2007-08-30
| | | | | | | + Formattage affichage arguments evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des redéfinitions de variables (définitions localesGravatar herbelin2007-08-29
| | | | | | | | | triviales en provenance de l'algo de compilation du filtrage) lors du calcul de la projection des variables dans real_clean git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10103 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
| | | | | | | | | échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding a few lemmas for reasoning about inequalities over the Gravatar roconnor2007-08-28
| | | | | | | rationals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans check_and_warnGravatar notin2007-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli dans la révision 10098 (nettoyage body_of_type)Gravatar herbelin2007-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des type_app et body_of_type qui alourdissent inutilement le codeGravatar herbelin2007-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug on wellfounded defs with constant parameters and dependencies on the ↵Gravatar msozeau2007-08-26
| | | | | | rec argument, example given by Brian Aydemir. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix de Bruijn bug in wf definitions.Gravatar msozeau2007-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add info on measure based defs.Gravatar msozeau2007-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix evars bug in mutual fixpoints with implicit types and bug in ↵Gravatar msozeau2007-08-26
| | | | | | inequalities generation for multiple patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add more equality tactics. Upgrade program_simpl for discrimination of ↵Gravatar msozeau2007-08-26
| | | | | | conjuncts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension et documentation de real_clean/evar_define dans evarutil.ml:Gravatar herbelin2007-08-25
| | | | | | | | | | | | | l'unification sait maintenant résoudre des équations du genre "?n[...;x:=?m[...;y:=t;...]] = t" lorsque x et y sont uniques vérifiant cette propriété (la solution est alors de poser ?m:=y et ?n:=x); le type de t est aussi pris en compte dans cette situation (ce genre de problème permet de résoudre des cas simples d'unification avec dépendance: cf l'exemple de foldrn dans test-suite/success/Fixpoint.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵Gravatar herbelin2007-08-24
| | | | | | -rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation plus précise de la contrainte de type pour interpréter lesGravatar herbelin2007-08-24
| | | | | | | | | | | points-fixes: on applique maintenant cette contrainte avant de généraliser corps et types vis à vis du context (utile notamment en présence de let-in dont on ne sait pas sinon s'ils font partie de la contrainte de type ou du contexte de typage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1634 + ajout de bugs dans la test-suiteGravatar notin2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
* Save IS NOT the same Defined ....Gravatar msozeau2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction bug dans syntaxe des match (liste de motifs vide était acceptée)Gravatar herbelin2007-08-22
| | | | | | | - Des open en plus dans le débogueur-traceur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un warning losrqu'un nom de bibliothèque est ambigüGravatar notin2007-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'initialisation des chemins de la librairie standardGravatar notin2007-08-20
| | | | | | | | | pour imposer un ordre précis des répertoires (résout en partie le problème entre Init.Wf et Program.Wf.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in INSTALL instructionsGravatar lmamane2007-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur de copier/coller dans la section GuardedGravatar notin2007-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1322Gravatar notin2007-08-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;Gravatar notin2007-08-16
| | | | | | | | | modification de interp_ltac_reference pour passer les ids utilisées dans le contexte d'appel d'une tactique. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10076 85f007b7-540e-0410-9357-904b9bb8a0f7
* An update on axiomatic number classes.Gravatar emakarov2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après ↵Gravatar notin2007-08-13
| | | | | | un commentaire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1635Gravatar notin2007-08-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un exemple d'inversion des dépendances dans le prédicat commeGravatar herbelin2007-08-10
| | | | | | | implicitement suggéré par le rapport de bug #1671 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10072 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un bug de de Bruijn dans abstract_predicate (lié auGravatar herbelin2007-08-10
| | | | | | | | | | | | rapport de bug #1671 - mais ne résoud pas le #1671 dans le propos peut être vu comme le souhait de voir traité le cas simple du problème généralement indécidable d'inversion des contraintes des types inductifs) - Petite amélioration dans le nommage des variables dans expand_arg git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10070 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar notin2007-08-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10069 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de la test suite pour intégrer des tests spécifiques auxGravatar notin2007-08-10
| | | | | | | | bugs soumis sur Coq-bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
| | | | | | | | | | | | iter_constr_with_full_binders + documentation de Guarded. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/doc/refman/RefMan-pro.tex M trunk/pretyping/inductiveops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix dependency bugs due to Program modules renamings.Gravatar msozeau2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vGravatar emakarov2007-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 10:51:24 +0000