aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/impargs.ml
Commit message (Collapse)AuthorAge
* Prevent automatic inference of implicit arguments when the auto flag isGravatar msozeau2009-06-01
| | | | | | | not set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
| | | | | | | | | | definitions and variables (may increase the vo's size a bit), which in turn fixes discharging with manual implicit args only. Fix Context to correctly handle "kept" assumptions for typeclasses, discharging a class variable when any variable bound in it is used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
| | | | | | | as they are used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
| | | | | | | | | | | | | | | - The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit nettoyage faisant suite au commit #11847 .Gravatar aspiwack2009-01-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Quelques modifications autour (géographiquement) de Util.list_split_at Util.list_split_at devient Util.list_split_when (dénomination inventée arbitrairement par moi-même, mais qui ne devrait pas déranger grand monde vu qu'il semble n'y avoir que deux occurences de cette fonction). Pour laisser la place à la fonction suivante : Introduction de Util.list_split_at: qui sépare la liste à une position donnée (alors que la nouvellement nommé list_split_when sépare à la première occurence "vrai" d'un prédicat). Ajout de quelques commentaires dans util.ml (pas le mli) sur ces deux fonctions. Suppression de Impargs.list_split_at (appel à Util). Suppression de Subtac_pretyping.list_split_at (qui était du code mort de toute façon). Suppression Util.list_split_by qui n'est utilisé nulle part et est une réimplémentation de List.partition (qui est probablement meilleure, en particulier tail-recursive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11851 85f007b7-540e-0410-9357-904b9bb8a0f7
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
| | | | | | | by the automatically infered arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11407 85f007b7-540e-0410-9357-904b9bb8a0f7
* broke cyclic dependenciesGravatar barras2008-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
| | | | | | | | | setting "Set Manual Implicit Arguments" for manual-only implicits. Fix test-suite script. This removes the discharge_info argument of "dynamic" object's rebuild function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix implicit arguments in sections bug and check for resolution of evars whenGravatar msozeau2008-07-07
| | | | | | | | | defining records. Fix test-suite script because of new implicit argument setting for DefaultRelation. Fix regression in auto, changing the order of tried lemmas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11213 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
| | | | | | | | | | | | | - Now [ id : Class foo ] makes id an explicit argument, and [ Class foo ] is equivalent to [ {someid} : Class foo ]. This makes declarations such as "Class Ord [ eq : Eq a ]" have sensible implicit args. - Better handling of {} in class and record declarations, refactorize code for declaring structures and classes. - Fix merging of implicit arguments information on section closing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11204 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
| | | | | | | | | | | | whether or not to keep them regardless of the actual dependencies (in order to implement the proper discharge behavior for type classes). This means adding an argument to rebuild_function in libobject, giving this information on variables after a section's constants have been discharged (discharge_function is too early). Surface syntax for Variable not added yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
| | | | | | | | | | | | | | | | | | works in inductive type definitions and fixpoints. The semantics of an implicit inductive parameter is maybe a bit weird: it is implicit in the inductive definition of constructors and the contructor types but not in the inductive type itself (ie. to model the fact that one rarely wants A in vector A n to be implicit but in vnil yes). Example in test-suite/ Also, correct the handling of the implicit arguments across sections. Every definition which had no explicitely given implicit arguments was treated as if we asked to do global automatic implicit arguments on section closing. Hence some arguments were given implicit status for no apparent reason. Also correct and test the parsing rule which disambiguates between {wf ..} and {A ..}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10677 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation des nouvelles options d'implicites (Set Strongly StrictGravatar herbelin2008-02-06
| | | | | | | | | | | Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de Set Strongly Strict Implicit : il contient maintenant Set Strict Implicit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10416 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
* 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
* Par compatibilité, les implicites terminaux sont maximaux aussi quandGravatar herbelin2007-05-22
| | | | | | | | inférés automatiquement (pas seulement si donnés manuellement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug calcul des implicites en présence d'evars dans les typesGravatar herbelin2007-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9827 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
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
| | | | | | | discharge_function des implicites au cas des scopes d'arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Avant : une unique méthode discharge_function qui avait accès à l'ancien environnement mais pas de possibilité de raisonner avec les objets du nouvel environnement en cours de construction. C'était problématique pour le discharge des implicites, arguments scope, etc qui étaient finalement faits en même temps que le discharge des constantes et inductifs mais avec pour effets de bord que les entrées dans la lib_stk arrivaient juste avant celles des constantes et inductifs avec des problèmes pour effacer les bonnes entrées au moment du reset - Maintenant : deux méthodes distinctes : discharge_function qui est appliquée pour collecter de l'ancien environnement ce qui est à garder dans la section et rebuild_function qui reconstruit le nouvel environnement connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant l'extensibilité que la méthode ancienne du fichier discharge.ml ne permettait pas) Au passage, ajout d'un modificateur Global aux déclarations d'implicites et d'arguments scopes pour indiquer qu'elles doivent perdurer à la sortie de la section Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps discharged reste) Au passage, nettoyage impargs.ml, suppression code mort résiduel du traducteur etc... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Évitement noms de constructeurs dans les motifs de filtrage de "match" (suite)Gravatar herbelin2006-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
| | | | | | | | | | (suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 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
* 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
* 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
* 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
* Moving centralised discharge into dispatched discharge_function; required to ↵Gravatar herbelin2005-02-18
| | | | | | delay some computation from before to after caching time + various simplifications and uniformisations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6748 85f007b7-540e-0410-9357-904b9bb8a0f7
* HUGE COMMITGravatar sacerdot2005-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement de iter_constr_with_full_binders dans TermopsGravatar herbelin2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4705 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de noms dans 'Implicit Arguments [...]'Gravatar herbelin2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'implicites par noms en v8Gravatar herbelin2003-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et ↵Gravatar herbelin2003-09-12
| | | | | | | | | choix du parseur en fonction de cette option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4255 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Affichage forcé des implicites contextuels si pas de contexte connuGravatar herbelin2003-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3910 85f007b7-540e-0410-9357-904b9bb8a0f7
* Synchronisation séparée des implicites pour l'affichage du traducteur;Gravatar herbelin2003-04-09
| | | | | | | différentiation aussi pour les Implicites manuels; nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction Show ImplicitsGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gestion synchronisation des Impargs.*_out et des Impargs._strict dans ImpargsGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3888 85f007b7-540e-0410-9357-904b9bb8a0f7
* Synchronisation avec resetGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3883 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
| | | | | | | | (notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des options "Set Contextual Implicits" et "Set Strict ImplicitsGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Analyse plus fine des occurrences rigidesGravatar herbelin2002-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte let-inGravatar herbelin2002-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3187 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des critères plus fins d'analyse des implicites automatiques; meilleur ↵Gravatar herbelin2002-10-28
| | | | | | affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:28:01 +0000