aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
Commit message (Collapse)AuthorAge
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
| | | | | | | | | | | | | | | | | | | | | | | files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
| | | | | | | | | | | | | | | | | | | name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Diverses corrections Gravatar herbelin2008-04-14
| | | | | | | | | | | | | | - gestion des idents (suite commit 10785) [lib, interp, contrib/ring, dev] - suppression (enfin) des $id dans les constr (utilisation des MetaIdArg des quotations de tactiques pour simuler les métas des constr - quitte à devoir utiliser un let-in dans l'expression de tactique) [proofs, parsing, tactics] - utilisation de error en place d'un "print_string" d'échec dans fourier - améliorations espérées vis à vis de quelques "bizarreries" dans la gestion des Meta [pretyping] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10790 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
| | | | | | | | | | | | | | | | | | | | | | - vérification de la cohérence des ident pour éviter une option -R avec des noms non parsables (la vérification est faite dans id_of_string ce qui est très exigeant; faudrait-il une solution plus souple ?) - correction message d'erreur inapproprié dans le apply qui descend dans les conjonctions - nettoyage autour de l'échec en présence de métas dans le prim_refiner - nouveau message d'erreur quand des variables ne peuvent être instanciées - quelques simplifications et davantage de robustesse dans inversion - factorisation du code de constructor and co avec celui de econstructor and co Documentation des tactiques - edestruct/einduction/ecase/eelim et nouveautés apply - nouvelle sémantique des intropatterns disjonctifs et documentation des pattern -> et <- - relecture de certaines parties du chapitre tactique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10785 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
| | | | | | | | Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
| | | | | | | | | | | | | | | | | | [in I] := t [return pred] in b", just as SSReflect does with let:. Change implementation: no longer a separate AST node, just add a case_style annotation on Cases to indicate it (if ML was dependently typed we could ensure that LetPatternStyle Cases have only one term to be matched and one branch, alas...). This factors out most code and we lose no functionality (win ! win !). Add LetPat.v test suite. - Slight improvement of inference of return clauses for dependent pattern matching. If matching a variable of non-dependent type under a tycon that mentions it while giving no return clause, the dependency will be automatically infered. Examples at the end of DepPat. Should get rid of most explicit returns under tycons. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is ↵Gravatar msozeau2008-01-17
| | | | | | backwards compatible. Update CHANGES with things i've done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalize instance declarations to any context, better name handling. Add ↵Gravatar msozeau2008-01-15
| | | | | | | | | hole kind info for topconstrs. Derive eta_expansion from functional extensionality axiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1749 (datant de l'implantation des or-patterns) +Gravatar herbelin2008-01-05
| | | | | | | | amélioration message d'erreur si nombre de pattern incorrect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de quelques défauts d'affichage (notations sous "as" pourGravatar herbelin2007-10-05
| | | | | | | | filtrage; sauts de line intempestifs dans pretty.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
| | | | | | | | | | | | | | | | | | | | the latter is bound to a var which is not a quantified one - this led to remove a line marked "temporary compatibility" ... ; made a distinction between quantified hypothesis as for "intros until" and binding names as in "apply with"; in both cases, we now expect that a identifier not used as a variable, as in "apply f_equal with f:=g" where "f" is a true binder name in f_equal, must not be used as a variable elsewhere [see corresponding change in Ints/Tactic.v]) - Fixing bug 1643 (bug in the algorithm used to possibly reuse a global name in the recursive calls of a coinductive term) - Fixing bug 1699 (bug in contracting nested patterns at printing time when the return clause of the subpatterns is dependent) - Fixing bug 1697 (bug in the TacAssert clause of Tacinterp.subst_tactic) - Fixing bug 1678 (bug in converting constr_pattern to constr in Constrextern) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10131 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Débogueur: positionnement de set_detype_anonymous pour ne pasGravatar herbelin2007-08-29
| | | | | | | | | échouer sur les Rel liées a des Anonymous et export de l'instance des evars vers le printeur du débogueur. - Suppression d'un reste de code mort lié à la V7 dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des types dans l'affichage des paramètres des (Co)Inductif/RecordGravatar herbelin2007-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte réversibilité des notations de la forme "Notation Nil := ↵Gravatar herbelin2007-05-10
| | | | | | | | | | @nil". Ajout @ref au niveau constr pour allègement syntaxe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9819 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
| | | | | | | | | | | | | discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - correction du mode strict qui n'était pas si strict, - option "Set Strong Strict Implicit" pour activer le mode strictement strict (désactivé par défaut pour raison de compatibilité), - option "Set Reversible Pattern Implicit" pour activer les implicites inférables par unification-pattern (désactivé par défaut par compatibilité), - option "Unset Printing Implicit Defensive" pour désactiver l'affichage des implicites n'ayant pas été décelés stricts, - option "Set Maximal Implicit Insertion" pour que les applications soient saturées en implicites si possible, - une optimisation du mode non strict pour que l'algo de recherche des implicites renonce à calculer les occurrences non strictes qui pourraient avoir à être affichées dans le mode défensif, avec pour conséquence que le mode défensif, pour celui qui le veut, devient a priori encore plus verbeux, ex: Set Implicit Arguments. Definition id x : nat := x. Parameter f : forall n, id n = id n -> Prop. Check (f (refl_equal O)). (* Affichait: "f (refl_equal 0)" mais affiche maintenant "f (n:=0) (refl_equal 0)" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug affichage des notations des noms de fonctions appliquéesGravatar herbelin2007-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a parameter to QuestionMark evar kind to say it can be turned into an ↵Gravatar msozeau2007-03-19
| | | | | | | | | | obligations (even an opaque one). Change cast_type to include the converted-to type or nothing in case of a Coerce cast, required much minor changes. Various little subtac changes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9718 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allègement de l'affichage des références par le printer si possibleGravatar herbelin2007-01-22
| | | | | | | | | | | | (on garde des noms de la forme IND(name,i) et CONSTR(name,i,j) que lorsqu'on ne sait pas le bon nom, i.e. pour les IND mutuels autres que le premier et pour tous les constructeurs). Pour un affichage complètement explicite des noms avec ocamldebug, charger maintenant set_raw_db en plus de db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option de débogage pour expliciter l'instance des evarsGravatar herbelin2007-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Variable print_instances pour déboguer les instances d'evarGravatar herbelin2006-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations:Gravatar herbelin2006-10-09
| | | | | | | | | | | | - prise en compte des variables liées non liées par la notation (bug #1186), - test pour affichage des notations aussi sur les sous-ensembles des lieurs multiples (cf notation "#" dans output/Notations.v), - extension, correction et uniformisation de quelques fonctions sur les constr_expr et cases_pattern (avec incidences sur rawterm.ml, parsing et contrib/interface). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Annulation de l'essai de changement de sémantique du %scope (révision 9208).Gravatar herbelin2006-10-06
| | | | | | | | | Retour à une sémantique où les %scope s'appliquent à la sous-expression complète (trop de pbs: constantes polymorphes sans arguments scope, variables locales de type fonctionnel, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
| | | | | | | | | | | | | | | | 1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer récursivement pour toutes les notations de l'expression concernée; 2- désactive la pile de scope pour cette notation immédiate. Le point 2 est clairement préférable pour les notations de la forme 3%sc, où on ne veut pas que 3 soit interprété dans un autre scope que sc même si sc n'a pas de notations numériques. Le point 1 est plus discutable et risque aussi de poser des incompatibilité (mais le comportement récursif peut être rétabli en changeant la valeur de quelques booléens marqués "recursive" dans constrextern.ml, constrintern.ml, et notation.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9208 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension des motifs disjonctifs au cas de disjonction de motifs multiplesGravatar herbelin2006-07-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added {measure x f} as a valid recursion order.Gravatar msozeau2006-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8831 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Distinction explicite des parties paramètres et arguments dans le typeGravatar herbelin2006-04-27
| | | | | | | | des inductifs de la clause "in" du filtrage. - Débogage et extension du parseur xml (g_xml.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8755 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
* - 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
* 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
* 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
* - Correction bug calcul mind_consnrealargs, introduit à la révisionGravatar herbelin2006-03-22
| | | | | | | | | | | | 7833, et que la révision 8644 n'avait pas corrigé dans le bon sens; renommage en mind_consnrealdecls pour éviter la confusion de sens avec mind_nrealargs - Correction de la description du type one_inductive_body - Ajout test avec let-in dans params et dans type constructeur (fichier Case12.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8653 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
* Version préliminaire d'inversion de la compilation du filtrageGravatar herbelin2006-01-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Résidus du traducteur v7 -> v8Gravatar herbelin2006-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 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
| | | | | | traitement dans alias de motifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ↵Gravatar herbelin2006-01-05
| | | | | | suppression des coercions permet aussi d'afficher un nombre, on choisit l'affichage qui n'introduit pas de délimiteurs si possible (exemple: avec 'Zpos 2', si Zpos est une coercion, on peut effacer la coercion et afficher 2 dans le type positive, ou bien garder la coercion afficher 'Zpos 2' comme 2 dans Z; dans certains cas - cf 4CT - il n'y a pas d'afficheur qui gère la coercion et il faut la retirer avant d'appliquer l'afficheur de nombre le plus interne) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des coercions non seulement avant l'affichage des notations mais ↵Gravatar herbelin2006-01-04
| | | | | | aussi avant l'affichage des notations primitives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux ↵Gravatar herbelin2005-12-30
| | | | | | de chaîne de caractères tel que "foo" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7762 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 des named_contextGravatar gregoire2005-12-02
| | | | | | | | Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug dé-globalisation syntactic def (cf coq-club 20/11/05)Gravatar herbelin2005-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7596 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Types inductifs parametriquesGravatar mohring2005-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage rawconstrGravatar herbelin2005-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6696 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-04 02:38:37 +0000