aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-07-04adding comments and cleaning code jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9003 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Typo dans le manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9002 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' ↵herbelin
+ modifs diverses de la présentation des règles d'inférence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9001 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04- completely new version of "functional inversion" using inversion onjforest
inductive - bug correction in "Functional scheme" and "functional inversion": the function are now parsed as references and not indent - adding a zeta normalization function in rawtermops to zeta normalize graph constructions (not used for now) - Bug correction in generation of functional principle types (if an arguments of the function has a type which is a sort) - adding a new persistent table for functional induction informations (graph,...) - new save mechanism for functional induction principles (reuse of proofs when possible) - Minor bug correction in proof of principle. - Distinguishing building_principles (that is save them) and making then (just construct their proof term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9000 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-04MAJ du manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8999 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Test des motifs disjonctifs multiplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8998 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Extension des motifs disjonctifs au cas de disjonction de motifs multiplesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03Mise à jour (avec retard) des niveaux de la table default_pattern_levelsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8996 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-03MAJ manuel de référencenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8995 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-29forgot a file jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8994 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-29bug correctionjforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8993 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-27Correction bug #1182 (ajout refresh_universe car le polymorphisme de sorte ↵herbelin
des inductifs maintenant retourne des sortes d'inductives qui ne sont pas des variables) et test de non-régression git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8992 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-27Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans ↵herbelin
l'environnement de preuve au moment de l'interprétation des arguments de tactiques (version 8971) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8991 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-26Ajout de Zgcd_spec (compat.)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8990 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-25nouvel algorithme pour Zgcd (plus rapide) + un Qcompareletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8989 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-25repetition d'hypotheses dans well_founded_induction_type_2letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8988 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Stricte positivité en présence de types inductifs imbriqués avec ↵herbelin
paramètres récursivement non uniformes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8987 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23modifs de test-suite suite au passage des graphes de Function dans Typejforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8986 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Passage des graphes de Function dans Type jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8985 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Fix wrong order of existentials in eterm.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8984 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8983 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Faire que les niveaux de tactiques soient correctement parsés par ARGUMENT ↵herbelin
EXTEND et TACTIC EXTEND git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8982 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suite passage ident -> hyp dans syntaxe de 'replace with in'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8981 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Nouveau paragraphe sur le polymorphisme de sorte des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8980 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suite utilisation hyp au lieu ident: donne la localisationnherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8979 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Mention de coqide, proof general et pcoqherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8978 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Correction ident -> hyp pour dinterpréter des identificateurs devant ↵herbelin
être interprétés comme termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8977 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Suppresion redondance interp_entry_name entre Q_util et Argextendherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8976 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-23Préservation compatibilité interprétation quantified hypothesis ↵herbelin
(provisoire ?) + export nouvelle macro pour maple.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8975 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-22Deux vérifications que le polymorphisme de sorte des inductifs ne ↵herbelin
fonctionne pas incorrectement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8974 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 12:44:16 +0000