aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-08-28Petite optimisation récursive-terminale en passantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9085 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-25two minor bug corrections in General Recursive Functions jforest
and one un structural Functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9084 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-25correction bug vm_computebgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9083 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24Morceau de code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9082 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9081 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9080 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9079 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24MAJ biblioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9078 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-24JMeq maintenant applicable sur Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9077 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-23Bug in replace tactics introduced in r9073 (overlap between replace .. with ↵jforest
and replace_term). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9076 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22making otags working jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9075 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22Forgot a file in previous commit jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9074 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and nojforest
InType) for "replace <c1> with <c2>" and "replace c1" and partially for "autorewrite". + Adding a "by tactic" optional argument to "setoid_replace". + Fixing bug #1207 + Add new test files for syntax change and updating doc. + Moving argument tactic extensions from extratactics to extraargs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9073 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-22remove an orphan comment (attached to a piece of code that was removed).bertot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9072 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-17Checks that abstract setoid rings can be defined in a module and the tacticbertot
can be used outside the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9071 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-17corrects an error in the substitution of module paths inside tactics:bertot
objects of the form TacDynamic should not be left unchanged if their content is tagged with "constr". This correction makes that setoid ring can now work with rings that were declared inside a module git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9070 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la ↵jforest
generation des graphes de Function + Correction d'un petit bug dans les lemmes d'inversions de Function + Nettoyage d'hypotheses inutile dans les obligations de preuve de Function (wf et measure). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9069 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-16MAJ Rectutorial (P. Castéran)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9068 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-15working on functional induction automation (tactic finduction andcourtieu
fauto, not documented yet) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9067 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-14comparison functions should be Defined not Qedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-11Bug corrections in Function.jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9065 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-08-08In the old version, recursive functions cannot be declared inside a sectionbertot
when the termination argument is based on the fact that some relation is well-founded. The goal correspond to the proof that the relation is well-founded is cleared of all useless hypotheses and variables, including variables that maybe used in the intermediary lemma that gathers all the proofs that need to be done interactively. As a result, this intermediary lemma cannot be re-used to prove this goal. The message is: Error: No such section variable or assumption : A This message appears at the time the user send the Qed command. This is problem report #PR1202 submitted by X. Leroy. The correction is to use the list of input variables to the function as the list of variables that should be cleared from the context. The function tclUSER_if_not_mes needs to be modified. This function is also used in contrib/funind/functional_principles_proofs.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9064 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28Modifications dans les scripts de configuration (coqtop et coqide affichent ↵notin
maintenant le numéro de révision svn) + correction problème OCaml 3.07 et caml_;odify git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9063 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28MAJ de la biblio du manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9062 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-28Reparation bug Show intros: les hypothèses introduites précédemmentcourtieu
dans le même paquet doivent être typables pour décider le nom des suivantes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9061 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-27Correction du bug #1170: les options synchronisées déclarées dans une ↵notin
section ne survivent plus à la fin de la section. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9060 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-26Modification script sed pour compatibilité Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9059 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-22- Ajout d'un cast vm dans la syntaxe : x <: t bgregoir
Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-20Correction du bug #1116 jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9057 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18amelioration du comportement de induction (retour a la version V8.0)jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9056 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18Correction bug #1192notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9055 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18Code cleaning in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9054 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-18Code cleaning in Functionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9053 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-17Renommage sqtr_lem_1 (bug 1189)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9052 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-17MAJjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9051 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-13bug correction when defining graph of fixpoints/definitions not generated by ↵jforest
F unction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9050 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-13Retrait du -noassert qui etait present en natif. letouzey
Ce -noassert empechait par exemple de s'apercevoir d'un echec actuel dans la test-suite. Heureusement les paquets debian faits par Samuel Mimram sont testés sur des tas d'archis, dont certaines en bytecode, ce qui a permis de reperer le bug. Pour que de telles blagues ne se reproduisent pas, il est essentiel que les asserts soient vérifiés y compris en natif. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9049 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-13Nombre magique pour la 8.1betaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9048 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-12Documentation machine virtuelleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9044 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-12Correction incohérence parsing de %delim dans les motifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9043 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵herbelin
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
2006-07-11Ajout de quelques Arguments Scope pour simuler la récursivité du scope ↵herbelin
romega_scope en compensation (et anticipation) d'une suppression de la récursivité des délimiteurs de scope (ici %term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9041 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11MAJ doc/refmannotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9040 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9039 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Documentation de lazymatch et des extensions de idtac et failherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9038 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-11Utilisation du mot-clé lazymatch pour le match paresseux (à défaut ↵herbelin
d'avoir trouver mieux) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9037 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-10+functional inversion now takes the function to invert as an optional argument. jforest
+ Code cleaning un Function code git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9036 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-09Argument Scope de list déplacé dans List.vherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9035 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de ↵herbelin
famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9033 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-07Correction bug 1172 + correction en passant de la taille des paramètres de ↵herbelin
famille git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9032 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 08:56:19 +0000