aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2007-08-29Prise en compte des redéfinitions de variables (définitions localesherbelin
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
2007-08-29- Débogueur: positionnement de set_detype_anonymous pour ne pasherbelin
é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
2007-08-28Adding a few lemmas for reasoning about inequalities over the roconnor
rationals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10101 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-28Correction d'un bug dans check_and_warnnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10100 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-27Oubli dans la révision 10098 (nettoyage body_of_type)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10099 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-27Suppression des type_app et body_of_type qui alourdissent inutilement le codeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Fix bug on wellfounded defs with constant parameters and dependencies on the ↵msozeau
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
2007-08-26Fix de Bruijn bug in wf definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10096 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Add info on measure based defs.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10095 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Fix evars bug in mutual fixpoints with implicit types and bug in ↵msozeau
inequalities generation for multiple patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10094 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-26Add more equality tactics. Upgrade program_simpl for discrimination of ↵msozeau
conjuncts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-25Extension et documentation de real_clean/evar_define dans evarutil.ml:herbelin
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
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵herbelin
-rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-24Utilisation plus précise de la contrainte de type pour interpréter lesherbelin
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
2007-08-22Correction du bug #1634 + ajout de bugs dans la test-suitenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10085 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-22Save IS NOT the same Defined ....msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10084 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-22- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)herbelin
- 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
2007-08-22Ajout d'un warning losrqu'un nom de bibliothèque est ambigünotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10082 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-20Modification de l'initialisation des chemins de la librairie standardnotin
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
2007-08-20Typo in INSTALL instructionslmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10080 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-20Erreur de copier/coller dans la section Guardednotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10079 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-16Correction du bug #1322notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10077 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
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
2007-08-13An update on axiomatic number classes.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10075 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-13Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après ↵notin
un commentaire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10074 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-13Correction du bug #1635notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10073 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-10Ajout d'un exemple d'inversion des dépendances dans le prédicat commeherbelin
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
2007-08-10- Correction d'un bug de de Bruijn dans abstract_predicate (lié auherbelin
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
2007-08-10Typonotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10069 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-10Modification de la test suite pour intégrer des tests spécifiques auxnotin
bugs soumis sur Coq-bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10068 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-09Modification de control_only_guard, qui utilise maintenantnotin
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
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10064 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-08Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vemakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10063 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-08Add a test case for the new "dependent" induction tactics.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10062 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10061 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Move Program tactics into a proper theories/ directory as they are general ↵msozeau
purpose and can be used directly be the user. Document them. Change Prelude to disambiguate an import of a Tactics module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10060 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Add a new tactic to generalize an instantiated inductive predicate adding ↵msozeau
equalities. Useful to do so-called "ford" induction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10059 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Build system: _really_ don't recurse into VCS metadata for file listslmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10058 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-07Build system:lmamane
- BSD compatibility: do not use -printf action of find (2nd round) - don't recurse into VCS metadata for file lists git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10057 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-01Build system: BSD compatibility: do not use -printf action of findlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10056 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-30mul and sqrtthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10055 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-26Corrected the reference to glob.dump, which is used to create ↵emakarov
stdlib/index-body.html. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10051 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-25Add glob.dump to Makefile the recommended way and document thelmamane
recommended way more explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10050 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-25Modifications de la construction de la documentation de la librairienotin
standard: - ajout d'une entrée dans le Makefile principal pour le fichier de globalisations glob.dump - modifications de doc/Makefile et de l'index html pour gérer les nouveaux fichiers de la librairie standard (en part. ceux dans Ints) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10049 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-25Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etnotin
do_norm. Corrigé par analogie avec N11, N12, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10048 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24fixed bug 1448 and 1674barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10046 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24proof of compare addedthery
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10045 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24fixed bug 1675: computing carrier from the relation type was not rightbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10043 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
Cleaner code: the guardedness bug is now corrected. Added "trivial" to the automation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10042 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-07-24An update on axiomatization of numbers.emakarov
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:06:52 +0000