aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Improved printing of Unfoldable constants in hints databases (usedGravatar herbelin2010-09-02
| | | | | | | user-level pr_constant instead of debugging-level pr_con + used ppnl and boxes instead of explicit fnl's so as not to disturb formatting). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13390 85f007b7-540e-0410-9357-904b9bb8a0f7
* r13359 continued: removed native treatment for λ (lambda) and Π (Pi)Gravatar herbelin2010-07-30
| | | | | | | | | | | what frees the tokens for other uses in non-unicode mode. For Π, users will have to introduce their own recursive notation. For λ, this is provided by the -unicode option (which actually is not documented nor as an option nor in the reference manual; maybe it should simply be now removed since "Require Import Utf8_core" has the same effect). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13359 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
| | | | | | requiring a file Utf8_core. That needs to be improved... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Constrintern: unified push_name_env and push_loc_name_env; madeGravatar herbelin2010-07-22
| | | | | | | | | | location dumping for binders uniformly treated in constrintern.ml (and renamed the optional arg of interp_context from fail_anonymous to global_level since the flag now also decides whether to dump binders as global or local ones); added locations for the variables occurring in the "as in" clauses; git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed parsing of "Generalizable Variable A" ("Variable" turns to be a keyword).Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish adding out-of-the-box support for camlp4Gravatar letouzey2010-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying François' patches about Canonical Projections (see #2302 and #2334).Gravatar herbelin2010-06-26
| | | | | | | Printer pr_cs_pattern is kept in recordops only. Also updated CHANGES. Fixed spelling of "uniform inheritance condition" in doc too (see git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13204 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using vernac parsing for FunctionGravatar jforest2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
* A new command Compute foo, shortcut for Eval vm_compute in fooGravatar letouzey2010-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13070 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added command "Locate Ltac qid".Gravatar herbelin2010-06-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13067 85f007b7-540e-0410-9357-904b9bb8a0f7
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
| | | | | | Still messy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
| | | | | | | | | | | | Cf tok.ml, token isn't anymore string*string where first string encodes the kind of the token, but rather a nice sum type. Unfortunately, string*string (a.k.a Plexing.pattern) is still used in some places of Camlp5, so there's a few conversions back and forth. But the penalty should be quite low, and having nicer tokens helps in the forthcoming integration of support for camlp4 post 3.10 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13018 85f007b7-540e-0410-9357-904b9bb8a0f7
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
| | | | | | Ocaml 3.10.0 is already three year old... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
* Missing warning flush in a lexer message + update of CHANGESGravatar herbelin2010-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13010 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fail: a way to check that a command is refused without blocking a scriptGravatar letouzey2010-04-30
| | | | | | | | | | | | | | | | | | | | | | | "Fail cmd" is similar to "Time cmd", but instead of printing the execution time, it reverse the exit status of cmd. "Fail cmd" is successful iff cmd has ended with an error. This was, we can demonstrate erroneous commands in a script for pedagogical or testing purpose without having to comment it in order to play the rest of the script in coqide/PG. Coq < Fail Foo. The command has indeed failed with message: => Error: Unknown command of the non proof-editing mode. Coq < Fail Check Prop. Prop : Type Error: The command has not failed ! Two more remarks: - Fail doesn't catch anomalies. - Yes it it possible to write things like Fail Fail ... :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12981 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed obsolete v7->v8 translation code (function check_same_type isGravatar herbelin2010-04-29
| | | | | | | costly in size but it is still used for checking that the parameters of mutual inductive types are the same...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
| | | | | | | | | | | | | | | | | | | dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc small fixes : warning, dep cycles, ocamlbuild...Gravatar letouzey2010-04-26
| | | | | | | | | | | | - git ignore g_decl_mode.ml - exhaustive match for pp_vernac (BeginSubproof, ...) - for ocamlbuild, remove a spurious cycle in recordops.mli (unnecessary open of Classops), and fixes of *.itargets and _tags The compilation via ocamlbuild still need some work, since plugin firstorder now depends on the new plugin decl_mode git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a fairly large commit (around 140 files and 7000 lines of code impacted), it will cause some troubles for sure (I've listed the know regressions below, there is bound to be more). At this state of developpement it brings few features to the user, as the old tactics were ported with no change. Changes are on the side of the developer mostly. Here comes a list of the major changes. I will stay brief, but the code is hopefully well documented so that it is reasonably easy to infer the details from it. Feature developer-side: * Primitives for a "real" refine tactic (generating a goal for each evar). * Abstract type of tactics, goals and proofs * Tactics can act on several goals (formally all the focused goals). An interesting consequence of this is that the tactical (. ; [ . | ... ]) can be separated in two tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for this particular syntax). We can also imagine a tactic to reorder the goals. * Possibility for a tactic to pass a value to following tactics (a typical example is an intro function which tells the following tactics which name it introduced). * backtracking primitives for tactics (it is now possible to implement a tactical '+' with (a+b);c equivalent to (a;c+b;c) (itself equivalent to (a;c||b;c)). This is a valuable tool to implement tactics like "auto" without nowing of the implementation of tactics. * A notion of proof modes, which allows to dynamically change the parser for tactics. It is controlled at user level with the keywords Set Default Proof Mode (this is the proof mode which is loaded at the start of each proof) and Proof Mode (switches the proof mode of the current proof) to control them. * A new primitive Evd.fold_undefined which operates like an Evd.fold, except it only goes through the evars whose body is Evar_empty. This is a common operation throughout the code, some of the fold-and-test-if-empty occurences have been replaced by fold_undefined. For now, it is only implemented as a fold-and-test, but we expect to have some optimisations coming some day, as there can be a lot of evars in an evar_map with this new implementation (I've observed a couple of thousands), whereas there are rarely more than a dozen undefined ones. Folding being a linear operation, this might result in a significant speed-up. * The declarative mode has been moved into the plugins. This is made possible by the proof mode feature. I tried to document it so that it can serve as a tutorial for a tactic mode plugin. Features user-side: * Unfocus does not go back to the root of the proof if several Focus-s have been performed. It only goes back to the point where it was last focused. * experimental (non-documented) support of keywords BeginSubproof/EndSubproof: BeginSubproof focuses on first goal, one can unfocus only with EndSubproof, and only if the proof is completed for that goal. * experimental (non-documented) support for bullets ('+', '-' and '*') they act as hierarchical BeginSubproof/EndSubproof: First time one uses '+' (for instance) it focuses on first goal, when the subproof is completed, one can use '+' again which unfocuses and focuses on next first goal. Meanwhile, one cas use '*' (for instance) to focus more deeply. Known regressions: * The xml plugin had some functions related to proof trees. As the structure of proof changed significantly, they do not work anymore. * I do not know how to implement info or show script in this new engine. Actually I don't even know what they were suppose to actually mean in earlier versions either. I wager they would require some calm thinking before going back to work. * Declarative mode not entirely working (in particular proofs by induction need to be restored). * A bug in the inversion tactic (observed in some contributions) * A bug in Program (observed in some contributions) * Minor change in the 'old' type of tactics causing some contributions to fail. * Compilation time takes about 10-15% longer for unknown reasons (I suspect it might be linked to the fact that I don't perform any reduction at QED-s, and also to some linear operations on evar_map-s (see Evd.fold_undefined above)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
| | | | | | | syntax of "Implicit Type" (that can now be "Implicit Types" and can now accept several blocks of variables of a given type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12960 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving error messages in the presence of utf-8 charactersGravatar herbelin2010-03-30
| | | | | | | | | | | | - A more clever strategy than the use of null spaces (in revision 12058) for collapsing multi-byte utf-8 characters into one character (toplevel.ml, 8.3 and trunk only) - Fixing discard_to_dot in the presence of iterated lexing failures - Made the lexer state aligned with the start of utf-8 chars instead of staying in the middle of multi-byte chars when a token is not recognized (lexer.ml4) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12891 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - make links to section variables working (used qualified names for disambiguation and fixed the place in intern_var where to dump them) (wish #2277) - mapping of physical to logical paths now follows coq (see bug #2274) (incidentally, it was also incorrectly seeing foobar.v as a in directory foo) - added links for notations - added new category "other" for indexing entries not starting with latin letter (e.g. notations or non-latin identifiers which was otherwise broken) - protected non-notation strings (from String.v) from utf8 symbol interpretation - incidentally quoted parseable _ in notations to avoid confusion with placeholder in the "_ + _" form of notation - improved several "Sys_error" error messages - fixed old bug about second dot of ".." being interpreted as regular dot - removed obsolete lexer in index.mll (and renamed index.mll to index.ml) - added a test-suite file for testing various features of coqdoc Things that still do not work: - when a notation is redefined several times in the same scope, only the link to the first definition works - if chars and symbols are not separated in advance, idents that immediately follow symbols are not detected (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}") - parentheses, curly brackets and semi-colon not linked in notations Things that can probably be improved: - all notations are indexed in the same category "other"; can we do better? - all non-latin identifiers (e.g. Greek letters) are also indexed in the same "other" category; can we do better? - globalization data for notations could be compacted (currently there is one line per each proper location covered by the notation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
| | | | | | | | (currently only one expansion but could be virtually made user-parametrizable). Also fixed a bug in recursive notations happening with multiple-tokens separators (see Notations.v in test-suite). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes in rewrite and a Elimination/Case to Scheme:Gravatar msozeau2010-03-06
| | | | | | | | | | | | | | - disallow dynamic generation of [case] constructs through [find_scheme] during a rewrite, as it changes the global environment and subsequent manipulations of the tactic may use an outdated environment. - use local exception names so as not to catch and hide unexpected [Not_found] exceptions. - fix lifting of constraints for dependent function types - Allow rewriting on morphisms (terms in function position) even with [rewrite] (fixes bug #2178). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form)Gravatar letouzey2010-03-04
| | | | | | | | | | | | | | | | - This way, the Makefile.build gets shorter and simplier, with a few nasty hacks removed. - In particular, we stop creating dummy .ml of .ml4 early "to please ocamldep". Instead, we now use ocamldep -modules, and process its output via coqdep_boot. This ways, *.cm* of .ml4 are correctly located, even when some .ml files aren't generated yet. - There is no risk of editing the .ml of a .ml4 by mistake, since it is by default in a binary format (cf pr_o.cmo and variable READABLE_ML4). M-x next-error still open the right .ml4 at the right location. - mltop.byteml is now mltop.ml, while mltop.optml keeps its name - .ml of .ml4 are added to .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12833 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
| | | | | | | | Let's avoid writing huge "Eval ... in ..." lines :-) Will be used in particular soon in NMake for defining function via Definition ... := Eval ... in ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
| | | | | | | | For F(X:T), the application !F M works as F M, except that if module type T contains some "Inline" annotations, they are not taken in account when substituting X with M in F. See forthcoming commits for examples of use for this feature. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7
* g_decl_mode: 'by' is now a keywordGravatar letouzey2010-01-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12660 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Segmenttree: New. A very simple implementation of segment trees.Gravatar regisgia2010-01-08
| | | | | | | | | | * Unicodetable: Update with the standard table for lower case conversion. * Util: Rewrite "lowercase_unicode" to take the entire unicode character set into account. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12645 85f007b7-540e-0410-9357-904b9bb8a0f7
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
| | | | | | | | Syntax Include Type is still active, but deprecated, and triggers a warning. The syntax M <+ M' <+ M'', which performs internally an Include, also benefits from this: M, M', M'' can be independantly modules or module type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
* "by" becomes officially a reserved keyword of Coq (fixes "rewrite ... at ... ↵Gravatar letouzey2010-01-06
| | | | | | | | by ...") Application in some proofs of Numbers's abstract division git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
| | | | | | | | | NB: the grammar entry is placed in vernac:command on purpose even if it should have gone into vernac:gallina_ext. Camlp4 isn't factorising rules starting by "Declare" in a correct way otherwise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
| | | | | | | | | | In trunk the different possible combinations of "at" and "in" with occurrences are taken into account. In 8.2 branch, it remains fragile (syntaxes that were accepted remain accepted and a message warns if the occurrences coming after the "with" are not taken into account). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12614 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing precedence while printing patterns in Ltac (was modified in r12607)Gravatar herbelin2009-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12611 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
| | | | | | | | | Class" too to handle references instead of just idents. Minor fix in coqdoc. zeta-normalize setoid_rewrite proofs, removing useless let-bindings generated by the tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We renounced to distribute evars to constr and bindings and to let tactics do the merge. There are now two disciplines: - the general case is that the holes in tactic arguments are pushed to the general sigma of the goal so that tactics have no such low-level tclEVARS, Evd.merge, or check_evars to do: - what takes tclEVARS and check_evars in charge is now a new tactical of name tclWITHHOLES (this tactical has a flag to support tactics in either the "e"- mode and the non "e"- mode); - the merge of goal evars and holes is now done generically at interpretation time (in tacinterp) and as a side-effect it also anticipates the possibility to refer to evars of the goal in the arguments; - with this approach, we don't need such constr/open_constr or bindings/ebindings variants and we can get rid of all ugly inj_open-style coercions; - some tactics however needs to have the exact subset of holes known; this is the case e.g. of "rewrite !c" which morally reevaluates c at each new rewriting step; this kind of tactics still receive a specific sigma around their arguments and they have to merge evars and call tclWITHHOLES by themselves. Changes so that each specific tactics can take benefit of this generic support remain to be done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Rewrite [classify_unicode] using standard unicode tables.Gravatar regisgia2009-12-20
| | | | | | | | (This should be a conservative extension of the old version.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12601 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made the interpretation levels rlevel/glevel/tlevel truly phantomGravatar herbelin2009-12-19
| | | | | | | types so that the type of terms in Genarg can be changed w/o in full independence of the level. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deactivating printing of {| |} for records when option Printing All is set.Gravatar herbelin2009-12-13
| | | | | | | Simplifying the printing of "in" clause keeping the same defaults as in parsing (e.g. "simpl" is printed "simpl" and not "simpl in *"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12582 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 23:06:17 +0000