aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Finalement, scopes utiles pour option 'where' (cf bug #1132)Gravatar herbelin2006-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8689 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
| | | | | | | | | | - Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8687 85f007b7-540e-0410-9357-904b9bb8a0f7
* versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmesGravatar letouzey2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8686 85f007b7-540e-0410-9357-904b9bb8a0f7
* ouverture du bon scope (positive_scope) derriere le constructeur Npos de NGravatar letouzey2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Enlevement de message d'erreur garbage.Gravatar courtieu2006-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
* resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses Gravatar letouzey2006-04-05
| | | | | | | | avec des equivalences parametrees (genre forall n, P n <-> Q n) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8683 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Licence FAQGravatar herbelin2006-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8682 85f007b7-540e-0410-9357-904b9bb8a0f7
* on utilise explicitement Prop/iff pour certains morphismes pour eviter des ↵Gravatar letouzey2006-04-05
| | | | | | warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression du test Proof with <tac>Gravatar notin2006-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8680 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'un rattrapage d'erreur pour "induction using".Gravatar courtieu2006-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug index addendum à cause mauvaise utilisation asection dans Helm.texGravatar herbelin2006-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 1119 (inversion marche a moitie dans Type)Gravatar herbelin2006-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8677 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite actualisation FAQGravatar herbelin2006-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amendement impression evar pour affichage des Meta par 'info'Gravatar herbelin2006-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8675 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réajout de eq_rec_eq oublié lors de la modularisation de EqdepGravatar herbelin2006-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductifs avec polymorphisme de sorte (version initiale)Gravatar herbelin2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout array_fold_map', list_fold_map' et list_remove_firstGravatar herbelin2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8672 85f007b7-540e-0410-9357-904b9bb8a0f7
* pour coqdocGravatar letouzey2006-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nommage explicite de certains "intro" pour préserver la compatibilitéGravatar herbelin2006-03-28
| | | | | | | | en préparation du passage à des inductifs à polymorphisme de sorte ("sigT R" va devenir de type le type de R, càd Set) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
* - correction d'un bug dans coqdoc (multi_index)Gravatar notin2006-03-28
| | | | | | | - modif. de la génération de la doc de stdlib git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug/typo dans splay_prod_assum et ajout decomp_sortGravatar herbelin2006-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8668 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des conflits Intmap/FSet FSets/FSet et Datatypes.Lt,Eq,Gt / ↵Gravatar letouzey2006-03-28
| | | | | | OrderedType.Lt,Eq,Gt git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8667 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:18:14 +0000