aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* Retour à un warning en cas de (co-)fixpoint pas totalement mutuelGravatar herbelin2006-09-09
| | | | | | | | | (après tout, d'autres exemples de non totalement mutuels sont acceptés sans problème par la test de bonne fondation - cf add1/add2 dans Sophia-Antipolis/MATHS/GROUPS/Z et Sophia-Antipolis/HARDWARE) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9128 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement, interdiction des points fixes non totalement mutuellementGravatar herbelin2006-09-06
| | | | | | | | | | | | | | récursifs parce ce que la condition de garde élimine les appels récursifs sur des sous-termes qui, par construction des types inductifs, ne peuvent ultimement retomber sur un objet du type initial de l'argument de décroissance (p.ex. un appel récursif sur p:positive provenant d'un filtrage sur un z:Z ne sera d'emblée pas considérer sous-terme car la destruction d'un positive ne donnera jamais un Z -- cf exemple de addZ dans une version d'avant aujourd'hui de Sophia-Antipolis/MATHS/GROUPS/Z/Zadd.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité clause "where" dans co-points fixes Gravatar herbelin2006-09-01
| | | | | | | (+ uniformisation position notation dans les blocs inductifs et récursifs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension et réorganisation de l'interprétation des (co-)points fixesGravatar herbelin2006-09-01
| | | | | | | | | | | | | | | | | | | | | | - Relâchement de l'exigence que les types des paramètres et le type des (co-)points fixes soient donnés. Ils peuvent maintenant être inférés à partir des autres informations de types. - Plus de déclaration séparée de celles des fonctions d'un bloc de points fixes qui n'interviennent pas dans la définition des autres (collect_non_rec): remplacement par un simple warning en cas de non dépendance mutuelle de toutes les fonctions du bloc (de toutes façons les fonctions qui intervenaient dans les autres sans en dépendre - càd les fonctions définissables avant la partie point fixe - n'étaient pas détectées) - Ajout du test de dépendance mutuel au cas des co-points fixes Extension et réorganisation de l'interprétation des blocs de définitions (co-)inductives: relâchement de l'exigence que les types des paramètres soient donnés. Ils peuvent maintenant être inférés à partir des autres informations des blocs d'inductifs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9108 85f007b7-540e-0410-9357-904b9bb8a0f7
* Indentation + typoGravatar notin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9104 85f007b7-540e-0410-9357-904b9bb8a0f7
* improve the amount of information given by the Ltac tactic debuggerGravatar bertot2006-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9092 85f007b7-540e-0410-9357-904b9bb8a0f7
* Morceau de code mortGravatar herbelin2006-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans les scripts de configuration (coqtop et coqide affichent ↵Gravatar notin2006-07-28
| | | | | | 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
* Correction du bug #1116 Gravatar jforest2006-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, ↵Gravatar herbelin2006-07-05
| | | | | | renommage en 'Set/Unset Ltac Debug' en prévision documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -with-geoproof à la configuration et à l'exécutionGravatar notin2006-06-09
| | | | | | | | 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
* Réinitialisation de token_number à chaque compilation d'un nouveau fichier ↵Gravatar notin2006-06-08
| | | | | | (fixe le bug #914) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8924 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation coqtop.mlGravatar notin2006-06-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de l'option -where: on vérifie si la variable d'environnement ↵Gravatar notin2006-06-07
| | | | | | COQLIB est définie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8912 85f007b7-540e-0410-9357-904b9bb8a0f7
* The "clean integration of subtac" patch.Gravatar msozeau2006-05-29
| | | | | | | | | | | | | Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle implantation du polymorphisme de sorte pour les familles inductivesGravatar herbelin2006-05-23
| | | | | | | | | | | - prise en compte du niveau à la déclaration du type comme une fonction des sortes des conclusions des paramètres uniformes - suppression du retypage de chaque instance de type inductif (trop coûteux) et donc abandon de l'idée de calculer une sorte minimale même dans des cas comme Inductive t (b:bool) := c : (if b then Prop else Type) -> t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8845 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanning and factorizing code in funind. Spliting new_arg_principles into ↵Gravatar jforest2006-05-03
| | | | | | to files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8781 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵Gravatar notin2006-04-28
| | | | | | 'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of emacs output: No more show script at the end of a proof.Gravatar courtieu2006-04-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8751 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of emacs output: Pp.warning and al now output warningGravatar courtieu2006-04-27
| | | | | | | | | | | between special characters. I had to add a hidden variable print_emacs and a function to set it to true in Pp because using Options.print_emacs would have introduce a circularity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8748 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
* 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
* 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
* 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
* - correction du bug #1055Gravatar notin2006-03-27
| | | | | | | | - modification des propriétés sur trunk et trunk/test-suite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8665 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 808: il est maintenant interdit de déclarer une ↵Gravatar coq2006-03-02
| | | | | | assomption en cours de preuve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug correction in saving proofs: If a hook opens a proof but does not close ↵Gravatar bertot2006-02-13
| | | | | | it then the delete_current_proof () does not delete the good proof if executed AFTER the hook. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Messages nth brancheGravatar herbelin2006-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration des messages d'erreurs de tacred; unfold considère maintenant leGravatar herbelin2006-02-07
| | | | | | | prédicat de filtrage après le terme filtré conformément à l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8003 85f007b7-540e-0410-9357-904b9bb8a0f7
* warning seulement si mode verboseGravatar herbelin2006-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7996 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas laGravatar herbelin2006-01-30
| | | | | | | bonne arité git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de la structure interne des types de déclarations (decl_kinds)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7941 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression code pour hints nommés à la V7 (voire à la V6...)Gravatar herbelin2006-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Messages de idtac et fail peuvent maintenant être des listes de string, int ↵Gravatar herbelin2006-01-21
| | | | | | et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7911 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar coq2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction dans vernac_exact_proof -- jmnGravatar coq2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1055Gravatar coq2006-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7862 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
| | | | | | | et d'"externalisation"; standardisation du nom des fonctions d'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7837 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de notations numérales définies au niveau utilisateur+ ↵Gravatar herbelin2006-01-08
| | | | | | légère restructuration + correction nécessité redéclarer syntaxe '{ _ }' dans le cas nouvelle notation basée sur '{ _ }' en -nois + suite nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7822 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation; suppression code mort; documentationGravatar herbelin2006-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7813 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement du commit incomplet de la révision 1.110 (cvs log ↵Gravatar herbelin2006-01-04
| | | | | | toplevel/metasyntax.ml) sur les formats de notations récursives + ajout de cassure par défaut en cas de notation récursive sans séparateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mini-restructurationGravatar herbelin2005-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Autres suppressions de composantes du traducteurGravatar herbelin2005-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des ↵Gravatar herbelin2005-12-26
| | | | | | G_*new en G_*.ml + autres petites modifications liées à suppression du traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7740 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des parseurs et printeurs v7; suppression du traducteur ↵Gravatar herbelin2005-12-26
| | | | | | (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de stratégie vis à vis du positionnement du module Top en mode ↵Gravatar herbelin2005-12-24
| | | | | | batch: si rien à compiler, on ouvre Top par défaut, pour l'éviter, il faut l'option -notop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction printer des Tactic NotationGravatar herbelin2005-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7709 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 16:48:49 +0000