aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-06-22Légère mise à jourherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8973 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Correction bug du polymorphisme de sort des inductifs (cas où les variables ↵herbelin
d'univers associées aux arités des paramètres ne sont pas distinctes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8972 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Nettoyage, uniformisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8971 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22updated documentation for my tactics (P. orbineaucorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8970 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Added {measure x f} as a valid recursion order.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Mutually structurally recursive defs and rec using measures added.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8968 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-21Harmonisation de l'interprétation des intropatternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8967 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Wellfounded recursion using subtac working again.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8966 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Progress in new wf def typing.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8965 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-20Rewrite of the recursive defs handling in progress.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8964 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-19bug serieux efficacite de ltacbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8963 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-16Ajout de tactiques expérimentales basée sur functional induction.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8962 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-15Report des modifications faites lors de la 8.0pl3 (ter)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8961 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-15Report des modifications faites lors de la 8.0pl3 (bis)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8960 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-15Report des modifications faites lors de la 8.0pl3notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8959 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-15Typo in case of reference to dev/doc/changes.txtlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8958 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8957 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8956 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-14A list of incompatibilitiesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8955 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-13ajout d'un argument with_clean a Indfun.functional_induction permettant de ↵jforest
choisir ou non de faire du menage dans les hypotheses engendrees. La tactique au niveau utilisateur fait toujours le menage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8954 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-13Changement du index.html généré dans refmannotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8953 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-13rearrangement du code: deplacement du code effectuant functionalcourtieu
induction vers indfun.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8952 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12Typo in replace doc. jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8951 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12Updating documentation of replace and correcting a typo in error message of ↵jforest
replace. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8950 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12changed comments.courtieu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8949 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-12git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8948 ↵jforest
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-10Bug is_numberherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8947 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-10MAJ fichier dev/doc/changes.txtherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8946 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-10ajout de la doc sur l'option -enable-geoproof de CoqIDEjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8945 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Suppression du répertoire distrib: il fait désormais partie du projet ↵notin
coq-dev-tools sur GForge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8943 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Commit doc Claudio Sacerdotiherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8942 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Nouvelle MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8941 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Déplacement vers archive coq-dev-tools/distribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8940 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Nouvelle MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8939 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09ajout de la doc de classical_right et leftjnarboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8938 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09MAJ liste fichiers doc stdlibherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8937 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Modification déf de exists! pour éviter une éta-expansion et pouvoir ↵herbelin
être filtré facilement par 'ex (unique ?P)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8936 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Adaptation Tactics.out et Cases.out au comportement actuel à défaut ↵herbelin
d'éviter l'affichage de trop d'espacements dans Tactics et de prendre une décision sur le rôle du _ dans Cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8935 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Bug suite déplacement Int.v dans ZArithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8934 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Déplacement Int.v dans ZArith, déplacement de DecidableType.v et ↵herbelin
DecidableTypeEx.v dans Logic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8933 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09Ajout d'une option -with-geoproof à la configuration et à l'exécutionnotin
pour inhiber la gestion de Geoproof sous Coqide (qui peut poser des problèmes avec GTK < 2.6.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8932 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09oups: il faut penser a fermer la porte en partant (d'un fixpoint)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8931 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-09changements de dernieres minutes pour la 8.1 beta: letouzey
- qualification correcte des noms en Haskell - on imprime les types de toutes les fonctions en Haskell - en Ocaml, les appels recursifs d'une f : 'a truc doivent se faire avec les _meme_ parametres de types 'a. Exemple illegal: let rec f = function [] -> 0 | l -> f [l];; On met maintenant des Obj.magic en conséquence. En Haskell (avec typage fourni), ca passe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8930 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Plus de Declare Module sans vrai type expliciteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8929 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08MAJ Makefile dependherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8928 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08nouvelle MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8927 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Changement du type d'argument 'TacticArgType X' en un typeherbelin
'ExtraArgType "tacticX"' (0<=X<=5) créé dynamiquement, ceci afin de pouvoir typer correctement les wit_tactic (auparavant le typage des wit_tactic était trop libéral et permettait de casser la subject-reduction). Amélioration au passage de l'affichage de la tactique "replace by" (module Extratactics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8926 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08MAJ coqc.byte et coqmktop.byteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8925 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵notin
(fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Warning ocaml 3.09 pour variable inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8923 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:24:26 +0000