aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
| | | | | | | | | | | | Fixed some bugs in -beautify and robustness of {struct} clause. Note: I tried to make the Automatic Introduction mode on by default for version >= 8.3 but it is to complicated to adapt even in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
| | | | | | | | | | Any place where <: was legal can now contain many <: declarations. Moreover we can say that the module type we are declaring is a subtype of an earlier module type. See DecidableType2 for examples. Also try to handle correctly the freeze/unfreeze summaries when simulating start/include/end (syntax ... := ... <+ ...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12532 85f007b7-540e-0410-9357-904b9bb8a0f7
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
| | | | | | | | | | | | | | | | | | | | "Module M (...) := M1 <+ M2 <+ M3 <+ ..." is now a shortcut for "Module M (...). Include M1. Include M2. Include M3... End M." Moreover M2,M3,etc can be functors as long as they find what they need in what comes before them (see new command "Include Self"). The only real constraint is that M1,M2,M3,... should not have common elements (for the moment (?)). Same behavior for signature : Module Type M := M1 <+ M2 <+ M3. Note that this <+ is _not_ a primitive construct of the module language, for instance it cannot be used in signature (Module M <: M1 <+ M2 is illegal for the moment). Some example of use in Decidable2 and NZAxioms git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12530 85f007b7-540e-0410-9357-904b9bb8a0f7
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If you have some Module Type F (X:Sig), and you are in a Module Type containing everything required to satisfy Sig (typically thanks to some earlier Include), then you can say Include Self Type F, and voila, objects of F are now added in your context, instantiated by local objects. Same behavior (hopefully) for modules and functors when using Include Self F. This experimental new command allows to easily produce static signatures out of functorial ones: Module Type F_static. Include Sig. Include Self F. End F_static. ... is similar to ... Module Type F_static. Declare Module X:Sig. Include F X. End F_static. ... but without the pollution of this artificial inner module X. This allow to split things in many othogonal components, and then mix them. It is a lightweight way to tackle the "diamond problem" of modular developpements without things like "overlapping" Include's (planned, but not yet there). See next commit for an example of use. Thanks to Elie for the debugging of my first ugly prototype... NB: According to Yann R.G., this is related with Scala's Traits. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12528 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
| | | | | | | | | [Generalizable (All|No) Variables (ident+)?], also update type classes documentation to reflect the latest changes in instance decls. Fix a bug in [Util.list_split_when]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
| | | | | | | | | | | | | | | | | | | | | | | | | | - Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes.Gravatar msozeau2009-11-06
| | | | | | | | | | | | | | - Correct backtracking function of coqdoc to handle the _p fields of lexers - Try a better typesetting of [[ ]] inline code considering it as blocks and not purely inline code like [ ] escapings. - Rework latex macros for better factorization and support external references in pdf output. - Better criterion for generalization of variables in dependent elimination tactic and better error message in [specialize_hypothesis]. - In autounfold, don't put the core unfolds by default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
| | | | | | | Fixed pretty printing of record syntax. Allowed record syntax inside patterns. (Patch by Cedric Auger.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Module type expressions of the form (Fsig X) with Definition foo := bar are ↵Gravatar soubiran2009-10-28
| | | | | | | | | | now accepted. +svn:ignore property on folders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12429 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
| | | | | | | | | - Clarification and documentation of the different styles of Local/Global modifiers in vernacexpr.ml - Addition of Global in sections for Open/Close Scope. - Addition of Local for Ltac when not in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
| | | | | | | | | of side conditions. Fix a small presentation issue in printing the "exists" tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12416 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed bug in Czar grammarGravatar corbinea2009-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
| | | | | | | | | | | | Implicit Arguments, Arguments Scope and Coercion fixed, noneffective Global in sections for Hints and Notation detected). Misc. improvements (comments + interpretation of Hint Constructors + dev printer for hint_db). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12411 85f007b7-540e-0410-9357-904b9bb8a0f7
* This big commit addresses two problems:Gravatar soubiran2009-10-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 1- Management of the name-space in a modular development / sharing of non-logical objects. 2- Performance of atomic module operations (adding a module to the environment, subtyping ...). 1- There are 3 module constructions which derive equalities on fields from a module to another: Let P be a module path and foo a field of P Module M := P. Module M. Include P. ... End M. Declare Module K : S with Module M := P. In this 3 cases we don't want to be bothered by the duplication of names. Of course, M.foo delta reduce to P.foo but many non-logical features of coq do not work modulo conversion (they use eq_constr or constr_pat object). To engender a transparent name-space (ie using P.foo or M.foo is the same thing) we quotient the name-space by the equivalence relation on names induced by the 3 constructions above. To implement this, the types constant and mutual_inductive are now couples of kernel_names. The first projection correspond to the name used by the user and the second projection to the canonical name, for example the internal name of M.foo is (M.foo,P.foo). So: ************************************************************************************* * Use the eq_(con,mind,constructor,gr,egr...) function and not = on names values * ************************************************************************************* Map and Set indexed on names are ordered on user name for the kernel side and on canonical name outside. Thus we have sharing of notation, hints... for free (also for a posteriori declaration of them, ex: a notation on M.foo will be avaible on P.foo). If you want to use this, use the appropriate compare function defined in name.ml or libnames.ml. 2- No more time explosion (i hoppe) when using modules i have re-implemented atomic module operations so that they are all linear in the size of the module. We also have no more unique identifier (internal module names) for modules, it is now based on a section_path like mechanism => we have less substitutions to perform at require, module closing and subtyping but we pre-compute more information hence if we instanciate several functors then we have bigger vo. Last thing, the checker will not work well on vo(s) that contains one of the 3 constructions above, i will work on it soon... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
| | | | | | | | | (see Notations.v). Improved the "already occurs in a different scope" test and message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removal of trailing spaces.Gravatar serpyc2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for Local Declare ML ModuleGravatar glondu2009-09-29
| | | | | | | Instead of failing with some obscure error message *after* loading the module, accept Local Declare ML Module with the usual semantics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Complement to 12347 and 12348 on the extended syntax of case/elim.Gravatar herbelin2009-09-27
| | | | | | | | | | | | | | | Don't change the semantics of "case 1" and forbid the use of numbers to refer to non-dependent quantified hypotheses in the more general forms that are synonymous of "destruct" (don't want to commit to a syntax for non-dependent quantified hypotheses which is ambiguous and after all not so appealing: for instance, something like destruct @1, destruct #1, or destruct at 1, or destruct :(ind_pattern), meaning in the latter case the first hypothesis whose type matches ind_pattern, would have probably been better). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add "case as/in/using" and temporary "destruct" with n args.Gravatar herbelin2009-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12347 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Addition of "Reserved Infix" continued.Gravatar herbelin2009-09-14
| | | | | | | | - Tried an extension of the lexer that supports keywords starting with a letter w/o being an ident (e.g. 'U+'). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12326 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
| | | | | | | | | | | | | | interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
| | | | | | | | | | | | | | | string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Postpone checking of Local/Global to allow grammar extensions to use itGravatar msozeau2009-09-02
| | | | | | | too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | Goptions). - Local Set/Unset ... change la valeur de l'option pour la section en cours (ou le module si il n'y a pas de section), l'option est restaurée à sa valeur précédente au sortir de la section. - Set/Unset ... survit aux sections mais pas aux modules. - Global Set/Unset ... survit aux sections et aux modules. Il y a une légère source d'incompatibilité là, Set avait le comportement de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on jamais. Les étapes suivantes : - Supprimer la notion d'option asynchrone, je n'en vois vraiment pas l'intérêt. Changer le type de retour de declare_option à unit aussi serait probablement une bonne idée. - Ajouter le support Local/Global à d'autres commandes sur le même modèle. Conflicts: parsing/g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added profile.cmo in grammar.cma so that any functions in one of theGravatar herbelin2009-08-14
| | | | | | files embedded in grammar.cma can be profiled with the Profile module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12279 85f007b7-540e-0410-9357-904b9bb8a0f7
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
| | | | | | | | | | only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
| | | | | | | | | in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain some minimal compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
| | | | | | | | - Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
| | | | | | | | | | | | - theories: made a hint database with the constructor of eq_true - coqide: binding F5 to About dans coqide + made coqide aware of string interpretation inside comments - lexer: added warning when ending comments inside a strings itself in a comment - xlate: completed patten-matching on IntroForthComing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow anonymous instances again, with syntax [Instance: T] where TGravatar msozeau2009-06-15
| | | | | | | may be a product. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12188 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
| | | | | | | | is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
| | | | | | | | | | | | | | - "*" implements Arthur Charguéraud's "introv" - "**" works as "; intros" (see also "*" in ssreflect). - Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui. - Shy attempt to seize the opportunity to clean Zarith_dec but Coq's library is really going anarchically (see a summary of the various formulations of total order, dichotomy of order and decidability of equality and in stdlib-project.tex in branch V8revised-theories). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
| | | | | | | instead of the index required by the user; extended FixRule and Cofix accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ensure the precondition of the partial function [list_chop] holdsGravatar msozeau2009-06-03
| | | | | | | before calling it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12162 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonctionGravatar aspiwack2009-05-28
| | | | | | | | | | | | qui permet de changer la façon dont on imprime certains sous-termes sans avoir à réécrire entièrement un printer de constr. Dans le même esprit que les commits sur le parser et le lexer, je cherche à donner une flexibilité aux plugins pour changer l'aspect de Coq pour le plier à d'autres conventions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12151 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dansGravatar aspiwack2009-05-27
| | | | | | | un plugin. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12147 85f007b7-540e-0410-9357-904b9bb8a0f7
* =?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Ma ↵Gravatar aspiwack2009-05-27
| | | | | | | | | | | | | | | | | lheureusement,=20je=20ne =20sais=20pas=20permettre=20que=20GDELETE=5FRULE=20soit=20appelable=20pendant=20une=20section =20sans=20causer=20de=20potentiels=20soucis=20(bien=20que=20je=20trouve=20qu'il=20faille=20un =20esprit=20sacr=C3=A9ment=20pervers=20pour=20faire=20Declare=20ML=20Module=20dans=20une=20section).?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit Je suppose qu'on est dans le même esprit d'information trop partielle que pour les notations aux niveaux 8, 99 et 200. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12146 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
| | | | | | | | | | | | | (bug 2092 and decl_mode.v in test suite). - Added a debugging printer for pftreestate. - Fixing American spelling in RefMan-decl.tex. - Optimizing application of tactic validation by removing consistency test in descend. - Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
| | | | | | | | | | | | | as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:57:16 +0000