aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
Commit message (Collapse)AuthorAge
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
| | | | | | | | | | | | | | | This permits to create a database [relations] in [RelationClasses] with a single extern tactic in it that tries to apply [reflexivity] or [symmetry]. This is then automatically used in [auto with *] and repair backward compatibility. The previous commit broke some scripts which were using [intuition] to do (setoid) [reflexivity] or [symmetry]: this worked only by accident, because the hint database of typeclasses was used. Overrall, this also allows to put a bunch of always-applicable, related tactics in some database or to use [Hint Extern] but match only on hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
| | | | | | | | | | making the auto apply entry. Makes indexing better and avoid polution of [auto with *] with many abstract lemmas comming from [typeclass_instances]. Quite a nice speedup again, even Field_theory has dropped to 58s from 70s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11381 85f007b7-540e-0410-9357-904b9bb8a0f7
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
| | | | | | | | | | | | | | | syntax yet. Doesn't change the auto/eauto behavior either. - Typeclass resolution now considers everything transparent by default and does it consistently for "open" and closed terms. - Correctly declare singleton classes definition as opaque for proof search. - Add a few initial declarations to make iff, id, compose... opaque - Add definition of dependent signatures for dependent function types and remove corresponding exception code in class_tactics. The instance requires higher-order unification and is not really usable yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11333 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
| | | | | | | | | | | | | | | classes, and simplify the implementation. - Experimental syntax {{ cl : Class args }} and (( cl : Class args )) which respectively make cl an implicit or explicit argument ({{ }} is equivalent to [ ]). Could be extended to any type of binder, eg. [Definition flip ((R : relation carrier)) : relation carrier := ...]. The idea behind double brackets is to distinguish macro-binders which perform implicit generalization from regular binders. It could also save [ ] for other uses. - Fix bug #1901 about {} binders in records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11210 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
* 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
* Strategy commands are now exportedGravatar barras2008-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
* refined the conversion oracleGravatar barras2008-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
| | | | | | | | | | | | | | | | | | | change the default pretty-printing to use Π, λ instead of forall and fun (and allow "," as well as "=>" for "fun" to be more consistent with the standard forall and exists syntax). Parsing allows theses new forms too, even if not in -unicode, and does not make Π or λ keywords. As usual, criticism and suggestions are welcome :) Not sure what to do about "->"/"→" ? - [setoid_replace by] now uses tactic3() to get the right parsing level for tactics. - Type class [Instance] names are now mandatory. - Document [rewrite at/by] and fix parsing of occs to support their combination. - Backtrack on [Enriching] modifier, now used exclusively in the implementation of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
| | | | | | | | | | | | | | binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Suppression d'une source de fuite mémoire dans declare_mod.ml (la table de hash library_table n'était pas synchronisée avec le reset et elle grossissait à chaque rejeu de la session; utilisation au passage d'une map pour que la synchronisation avec le reset soit plus rapide). [mod_typing.ml] - Correction d'un bug de synchronisation pour le niveau pattern 200. [pcoq.ml4] - Suppression d'un vieux reste du traducteur [constructeur VernacVar] - Robustesse et uniformité accrue dans CoqIDE vis à vis du statut de chacune des commandes vernaculaires par l'utilisation d'une fonction d'assignation d'attributs à chaque commande vernac. Correction de ce qui semble être des bizarreries (VernacDeclareTacticDefinition considéré comme ouvrant un but; suppression des "loc" dans les Reset: ne pouvait pas faire fonctionner correctement update_on_end_of_segment). Suppression de la nécessité d'expliciter si une commande retourne des messages dépendants du mode "verbose" (on suppose que chaque commande sait ce qu'elle doit dire selon la position du flag verbose). Sinon, le mécanisme de Reset de CoqIDE reste pauvre. CoqIDE ne sait revenir qu'aux états associés à des noms et cela ne vaut pas l'approche de Proof General. Il sera sans doute opportun de se brancher sur l'architecture de Pierre Courtieu à base de "Backtrack". La restriction des buts imbriqués a-t-elle vraiment une raison d'être ? En plus les commandes non cablées en dur comme Next Obligation ne sont pas prises en compte. Interdiction, dès Coq, d'ouvrir sections ou modules si preuve en cours. Réparation approximative de l'option "Help for Keyword" de Coqide mais encore à faire pour plus de robustesse (makefile, installation, synchronisation entre la version du fichier index_urls.txt et la version du refman, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10904 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
| | | | | | | | | | | des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | de l'argument donné contient des métavariables (souhait #1408). Beaucoup d'infrastructure autour des constantes pour cela mais qu'on devrait pouvoir récupérer pour analyser plus finement le comportement des constantes en général : 1- Pour insérer les coercions, on utilise une transformation (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml. 2- Pour la compatibilité, on s'interdit d'insérer une coercion entre classes flexibles parce que sinon l'insertion de coercion peut prendre précédence sur la résolution des evars ce qui peut changer les comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN). 3- Pour se souvenir rapidement de la nature flexible ou rigide du symbole de tête d'une constante vis à vis de l'évaluation, on met en place une table associant à chaque constante sa constante de tête (heads.ml) 4- Comme la table des constantes de tête a besoin de connaître l'opacité des variables de section, la partie tables de declare.ml va dans un nouveau decls.ml. Au passage, simplification de coercion.ml, correction de petits bugs (l'interface de Gset.fold n'était pas assez générale; specialize cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml]; whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml]) et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml, classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10840 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
| | | | | | | | | | | | semantics. - Add an Equivalence instance for pointwise equality from an Equivalence on the codomain of a function type, used by default when comparing functions with the Setoid's ===/equiv. - Partially fix the auto hint database "add" function where the exact same lemma could be added twice (happens when doing load for example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 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
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
| | | | | | | | | | | | | | | | | | | - Better interface in constrintern w.r.t. evars used during typechecking - Add "unsatisfiable_constraints" exception which gives back the raw evar_map that was not satisfied during typeclass search (presentation could be improved). - Correctly infer the minimal sort for typeclasses declared as definitions (everything was in type before). - Really handle priorities in typeclass eauto: goals produced with higher priority (lowest number) instances are tried before other of lower priority goals, regardless of the number of subgoals. - Change inverse to a notation for flip, now that universe polymorphic definitions are handled correctly. - Add EquivalenceDec class similar to SetoidDec, declaring decision procedures for equivalences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | | binding, add "!" syntax for the new binders which require parameters and not superclasses. Change backquotes for curly braces for user-given implicit arguments, following tradition. This requires a hack a la lpar-id-coloneq. Change ident to global for typeclass names in class binders. Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C t1 tn ]. Update affected theories. While hacking the parsing of { wf }, factorized the two versions of fix annotation parsing that were present in g_constr and g_vernac. Add the possibility of the user optionaly giving the priority for resolve and exact hints (used by type classes). Syntax not fixed yet: a natural after the list of lemmas in "Hint Resolve" syntax, a natural after a "|" after the instance constraint in Instance declarations (ex in Morphisms.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
| | | | | | | | | | - New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for substructures in classes using :> notationGravatar msozeau2008-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change notation for setoid inequality, coerce objects before comparing them. ↵Gravatar msozeau2008-01-18
| | | | | | Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 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
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but ↵Gravatar msozeau2008-01-07
| | | | | | implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 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
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
| | | | | | | | | | | | | - Le code est maintenant mieux commenté. - J'ai aussi réorganisé un petit peu pour le rendre plus léger, mais presque rien - j'ai changé les noms internes : needed_assumptions devient assumptions et PrintNeededAssumptions devient PrintAssumptions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of the Scheme command.Gravatar vsiles2007-09-28
| | | | | | | | | | | | Now you can forget to provide the name of the scheme, it will be built automatically depending of the sorts involved. e.g. Scheme Induction for nat Sort Set. will build nat_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of VernacScheme to handle a new scheme: Equality (equality inGravatar vsiles2007-05-25
| | | | | | | | | | | | | | | | | boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 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
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)Gravatar herbelin2007-02-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9678 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
* Addition of a "Combined Scheme" vernacular command for building the ↵Gravatar msozeau2006-12-23
| | | | | | | | | conjunction of mutual inductions principles. e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 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
* 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
* 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
* 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
* 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
* - debugging og "Show Intros": no line breaking + fresh idsGravatar coq2005-11-08
| | | | | | | | - added the command "Show Match t" which prints a typical "match...with" for type t. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7532 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command: "Print Ltac qualid" to print user defined tactics.Gravatar sacerdot2005-05-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence ↵Gravatar herbelin2005-05-17
| | | | | | aux niveaux syntaxiques des tacticielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implementation of a new backtracking system, that allow to go backGravatar coq2005-04-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | anywhere in a script (provided no suspend/resume is used): * the command "Backtrack n m p" (vernac_bactrack) performs the following operation: ** do abort p times, ** do undo on the current proof (after the aborts) in order to reach a stack depth of m (see vernac_undo_todepth) ** resets the global state to state labelled with n. * The coq prompt in emacs mode has more informations, it contains: ** the usual coq prompt plus: ** the state number (global state label) ** the depth of the current proof stack ** the names of all pending proofs, in *unspecified* order, separated by '|' Example: state proof stack num depth __ _ aux < 12 |aux|SmallStepAntiReflexive| 4 < ù ^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^ usual pending proofs usual special char git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming Print Canonical Structure into Print Canonical ProjectionsGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Print Canonical StructuresGravatar herbelin2005-02-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la syntaxe du reset label: "BackTo n".Gravatar coq2005-01-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6590 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
| | | | | | | | | | | | | | | | | * "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-26 08:44:50 +0000