aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* préparation de add_glob en vue d'isolement de la partie module pourGravatar herbelin2006-04-27
| | | | | | | l'option glob-dump git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8746 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout chop_dirpathGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8745 85f007b7-540e-0410-9357-904b9bb8a0f7
* 2-3 lemmes en plus pour que les Bvectors soient effectivement utilisablesGravatar letouzey2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a short doc for "Function". To be finished.Gravatar courtieu2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8743 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8742 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Utilisation d'abbréviations pour les types intervenant dans RCasesGravatar herbelin2006-04-26
| | | | | | | | | - Factorisation du procédé de transformation Cases -> RCases dans Detyping - Rebranchement de la traduction XML pour Cases (interrompue depuis suppression traducteur) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Outil de test de la réversibilité du réafficheur v8->v8Gravatar herbelin2006-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses corrections de l'afficheur et du traducteur pour s'assurer deGravatar herbelin2006-04-26
| | | | | | | | | | la réversibilité de la traduction (correction enregistrement des retours chariot dans le lexeur, correction affichage espace superflu en tête des VERNAC EXTEND, correction affichage morphism_signature dans extraargs.ml4, correction affichage clear dans pptactic.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Régénération après mise à jour coqdep pour traiter Require multipleGravatar herbelin2006-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte du Require multipleGravatar herbelin2006-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8737 85f007b7-540e-0410-9357-904b9bb8a0f7
* suite du pont entre Bvector et NGravatar letouzey2006-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing "GenFixpoint" with "Function" and "mes" with "measure"Gravatar jforest2006-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la ↵Gravatar notin2006-04-26
| | | | | | création du fichier de style git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un gros coup de lifting pour IntMap: Gravatar letouzey2006-04-25
| | | | | | | | | | | | | | | | | | | | | | * le type ad des adresses est maintenant un alias vers le N de NArith, qui lui est isomorphe. * toutes les operations sur ces adresses (p.ex. un xor bit a bit) sont maintenant dans de nouveaux fichiers du repertoire NArith. * Intmap utilise maintenant le meme type option que le reste du monde * etc etc... Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs utilisant Intmap sont adaptees en consequence. Me demander si besoin ma moulinette d'adaptation (incomplete). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
* un lemme de double inclusionGravatar letouzey2006-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverting nf_betaiotaevar_preserving_vm_castGravatar jforest2006-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8731 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mort (suite)Gravatar herbelin2006-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression code mortGravatar herbelin2006-04-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8729 85f007b7-540e-0410-9357-904b9bb8a0f7
* Timide tentative de clarification du statut de l'opérateur de filtrageGravatar herbelin2006-04-24
| | | | | | | | | | | | | | | PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement anomaly en failwith dans out_name pour utilisation par map_succeedGravatar herbelin2006-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;Gravatar herbelin2006-04-24
| | | | | | | | petites améliorations de l'afficheur de ltac match context (moins de parentheses, plus de structure) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8726 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Handling "if" and cast in GenFixpoint Gravatar jforest2006-04-24
| | | | | | | | | + Correcting a bug in recursives funcitons detection in GenFixpoint + Parially handling applied binders in funcitonal principles generation tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8725 85f007b7-540e-0410-9357-904b9bb8a0f7
* decoration des Tdummy pour pouvoir tuer tous les args de types (cf MapAVL.empty)Gravatar letouzey2006-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
| | | | | | | | | | | foncteurs sont données un par un ce qui permet de faire les load_objects correspondants au bon moment (càd juste après l'ajout des déclarations logiques et avant l'ajout du paramètre suivant). Ceci clôt le bug #1118 et corrige des erreurs de localisation introduite par le commit précédent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added code to support "Program Lemma/Example... etc"Gravatar msozeau2006-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8722 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
| | | | | | | | | | | | | | | | | | | | | à la déclaration des paramètres de foncteurs (problème de synchronisation révélé par bug #1118, apparu suite à l'appel de lookup_mind par load_struct, suite au passage à un discharge local) Les objets non logiques sont maintenant chargés après car ils peuvent dépendre d'objets logiques. Et comme les objets non logiques (p.ex. l'import récursif de modules dans la nametab) sont nécessaires au typage de l'éventuelle contrainte de module, on reporte la gestion de la contrainte au moment du end_module (on aurait peut-être pu faire plus fin et extraire dans do_module la partie purement module, mais après tout le report de la contrainte de type dans le end_module ne semble pas génante). À la date d'aujourd'hui, le bug #1118 reste toutefois ouvert avec les définitions de module non interactives. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tests notationsGravatar herbelin2006-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8720 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test synchronisation chargement objets non logiquesGravatar herbelin2006-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Si un fixpoint a plusieurs arguments, mais un seul de type inductif, Gravatar letouzey2006-04-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas fierGravatar herbelin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8717 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour creditsGravatar cpaulin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8716 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enleve les commentairesGravatar cpaulin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test files for subtac.Gravatar msozeau2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8714 85f007b7-540e-0410-9357-904b9bb8a0f7
* Maj configure, README, etc...Gravatar notin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Premier jet annonce 8.1Gravatar herbelin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8710 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 8.1Gravatar herbelin2006-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8709 85f007b7-540e-0410-9357-904b9bb8a0f7
* replacing whd_betaiotaevar_preserving_vm_cast Gravatar jforest2006-04-14
| | | | | | | by nf_betaiotaevar_preserving_vm_cast. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8708 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 8.1-APPGravatar herbelin2006-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8707 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 8.1-APPGravatar herbelin2006-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8706 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de licence pour le Tutoriel de CoqGravatar notin2006-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8703 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the proof of principlesGravatar jforest2006-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8702 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction on multiple arguments made better:Gravatar courtieu2006-04-12
| | | | | | | - dealing with arguments depending one on another - cleaning letins created during induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8701 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of "Show Intros": it now shows letins too.Gravatar courtieu2006-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8700 85f007b7-540e-0410-9357-904b9bb8a0f7
* adding a new tactic [intro_avoiding idl] which acts as intro but prevents theGravatar jforest2006-04-11
| | | | | | | new identifier to bellong to [idl] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8698 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'entrées dans TODO et CHANGES (à re-mettre à jour avant la release)Gravatar courtieu2006-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8697 85f007b7-540e-0410-9357-904b9bb8a0f7
* patch pour contourner l'échec de type_of_applied_inductive sur un inductif ↵Gravatar herbelin2006-04-11
| | | | | | appliqué à des meta non castés (à défaut de comprendre comment gérer le flux de typage des metas : besoin du type de l'inductive pour caster les metas arguments directs mais besoin de caster les metas arguments directs pour connaitre le type d'un inductif à polymorphisme de sorte) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8696 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for new unification, not used in default version as it really changes ↵Gravatar msozeau2006-04-10
| | | | | | unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8695 85f007b7-540e-0410-9357-904b9bb8a0f7
* + Changing a little functional schemes types Gravatar jforest2006-04-10
| | | | | | | | | | | | + New tactic to prove functions schemes + Add a command "Generate graph for <functionname>" to generate automatiquelly the graph associated to a function (usefull only when the function has not been defined by GenFixpoint). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8694 85f007b7-540e-0410-9357-904b9bb8a0f7
* Actual fix for the unification problem in theories/Reals/Rtrigo_fun ↵Gravatar msozeau2006-04-10
| | | | | | | | | | | (previous and current version work). Changed the type of typing constraints so as to have all the necessary information on abstract tycons. Updates of subtac to use the new type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
* New unification can solve the problem without eta-expansion, Gravatar msozeau2006-04-10
| | | | | | | but is bugguy with it. Temporary fix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8691 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 03:28:55 +0000