aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
* Hopefully complying with camlp5 < 6.00 syntaxGravatar herbelin2012-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Yet another subtlety with bug 2732: when several grammar rules of aGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | TACTIC EXTEND block possibly parse the stand-alone name of a tactic, then only the first rule must be registered in the atomic tactic table so as to be consistent with what happens when the tactic is invoked directly via its parsing rules and not via the interpretation of a reference in the atomic tactic table. Concretely, this affects TACTIC EXTEND blocks of the form TACTIC EXTEND foo [ "bar" tactic_opt(tac) -> ... ] | [ "bar" constr_list(tac) -> ... ] where both rules parses "bar" alone but only the first rule must be registered in the atomic table, git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | "f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an Ltac function - see Tacinterp.add_primitive_tactic). More precisely, when parsing "f ref" and "ref" is recognized as the name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic (like "eauto", "firstorder", "discriminate", ...), the code was correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END' was given (where "foo" has no arguments in the rule) but not when a rule of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given (where "foo" had an optional argument in the rule). In particular, "firstorder" was in this case. More generally, if, for an extra argument able to parse the empty string, a rule `TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given, then "foo" was not recognized as parseable as an atomic string (this happened e.g. for "eauto"). This is now also fixed. There was also another bug when the internal name of tactic was not the same as the user-level name of the tactic. This is the reason why "congruence" was not recognized when given as argument of an ltac (its internal name is "cc"). Incidentally removed the redundant last line in the parsing rule for "firstorder". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Final part of moving Program code inside the main code. Adapted ↵Gravatar msozeau2012-03-14
| | | | | | add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
| | | | | | | | | Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the syntax of pattern matching, "in" clauses are patterns.Gravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments supports extra notation scopesGravatar gareuselesinge2012-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
* A "Grab Existential Variables" to transform the unresolved evars at the end ↵Gravatar aspiwack2012-02-07
| | | | | | of a proof into goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix camlp4 compilationGravatar pboutill2012-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14951 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an pattern / occurence syntax for vm_compute.Gravatar ppedrot2012-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14950 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed a seemingly unused argument in Require of modules, introduced 10 ↵Gravatar ppedrot2012-01-23
| | | | | | years ago and absent from both coq and contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14937 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed pretty-printing of Opaque, Transparent and Strategy locality flags.Gravatar ppedrot2012-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14936 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted previous commit, which broke library compilation.Gravatar ppedrot2012-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14925 85f007b7-540e-0410-9357-904b9bb8a0f7
* This is a quick hack to permit the parsing of the locality flag in the ↵Gravatar ppedrot2012-01-20
| | | | | | Program subtactic. Ideally, locality flags should be handled in a nicer way... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14924 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix printing of classesGravatar msozeau2012-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14923 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.Gravatar msozeau2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pretty printing of generalized binderGravatar pboutill2012-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the pretty-printing of the Program plugin.Gravatar ppedrot2012-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some fix in beautify pretty-printerGravatar pboutill2012-01-17
| | | | | | | | | - In binders, {X} were printed X - Notation toto x y := were printed Notation totox y - Fixpoint declaration prints too much spaces Hunt is not closed yet anyway... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductiveops.nb_*{,_env} cleaningGravatar pboutill2012-01-16
| | | | | | | - Functions without _env use the global env. - More comments about when letin are counted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14908 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix printing of instances, generalized arguments.Gravatar msozeau2012-01-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed some printing details for dependent evars in emacs mode. PatchGravatar courtieu2011-12-19
| | | | | | | | | | | | | | | | from Hendrik Tews: 1) Print the dependent evars after "No more subgoals" and after "No more subgoals but non-instantiated existential". This is necessary to correctly display the instantiation status of dependent evars, because the last proof command might change them. 2) Change the ``Show Goal "id"'' command to include a header like goal / evar 2 is: This is more consistent with the other Show commands. Moreover it simplifies the use of this command in Proof General, because, with the change, the output contains the goal ID. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14824 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applied patches proposed suggested by Hendrik Tews to fix existentialGravatar courtieu2011-12-18
| | | | | | | | variables printing in emacs mode (put them at the end of input, and fix commas). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14818 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing PrintConstr debugging entry in g_proof.ml4 which was notGravatar herbelin2011-12-18
| | | | | | | working and was causing a warning when declaring the entry of same name in top_printers.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14815 85f007b7-540e-0410-9357-904b9bb8a0f7
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
| | | | | | | | | | as to ensure the warning is flushed in real time. Made systematic the use of if_warn instead of if_verbose when the warning is intended to signal something anormal (if_warn is activated when compiling verbosely and when working interactively while if_verbose is activated only when working interactively and when loading verbosely). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14803 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving pretty-printing of Ltac functions.Gravatar herbelin2011-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14801 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing previous commit which was bugging on tactics preceded by goal number ↵Gravatar courtieu2011-12-16
| | | | | | (2:intros.). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving bullets (-, +, *) into stand-alone commands instead of beingGravatar courtieu2011-12-16
| | | | | | | | part of a tactic. WARNING: Coqide needs to be adapted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14794 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proof using ...Gravatar gareuselesinge2011-12-12
| | | | | | | | | | | | | New vernacular "Proof using idlist" to declare the variables to be discharged at the end of the current proof. The system checks that the set of declared variables is a superset of the set of actually used variables. It can be combined in a single line with "Proof with": Proof with .. using .. Proof using .. with .. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Makefile: force the installation of all .cmi (and remove some obsolete .mli)Gravatar letouzey2011-12-08
| | | | | | | The previous code wasn't detecting and installing .cmi coming from .mli without corresponding .ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14783 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing grammar resetting bug in the presence of levels initially emptyGravatar herbelin2011-12-07
| | | | | | (the number of entries to reset was not correct). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14778 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
| | | | | | | | | | | | | | | | - Implicit arguments can be mentioned anonymously: Arguments map {_ _} f l. - To rename implicit arguments, the ": rename" flag must be used: Arguments map {T1 T2} f l : rename. Without the ": rename" flag arguments can be used to assert that a function has indeed the expected number of arguments and that the arguments are named as expected. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing superflous newline in output of About when no parameter is renamed.Gravatar herbelin2011-12-04
| | | | | | | | | Fixing output tests after having added flushing of warning in revisions 14747 and 14750. Moving Implicit output test to new command Arguments. Adding test of new Arguments syntax in PrintInfos.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r14747 being actually incomplete (flushing warnings andGravatar herbelin2011-11-30
| | | | | | printing them only if verbose). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14750 85f007b7-540e-0410-9357-904b9bb8a0f7
* Preventing Implicit Arguments warning to be shown in non verbose modeGravatar herbelin2011-11-30
| | | | | | + flushing printing of the message . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14747 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* In emacs mode, prints a list of the dependent existential variables introducedGravatar aspiwack2011-11-23
| | | | | | | | during the proof together with information whether they were (partially) instantiated and if it's the case the list of existential variables that were used to that effect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21
| | | | | | | | Example: Arguments eq_refl {B y}, [B] y. Check (eq_refl (B := nat)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
* New Arguments vernacularGravatar gareuselesinge2011-11-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The new vernacular "Arguments" attaches to constants the extra-logical piece of information regarding implicit arguments, notation scopes and the behaviour of the simpl tactic. The About vernacular is extended to print the new extra logical data for simpl. Examples: Arguments foo {A B}%type f [T] x. (* declares A B and T as implicit arguments, A B maximally inserted. declares type_scope on A and B *) Arguments foo {A%type b%nat} p%myscope q. (* declares A and b as maximally inserted implicit arguments. declares type_scope on A, nat_scope on b and the scope delimited by myscope on p *) Arguments foo (A B)%type c d. (* declares A and b in type_scope, but not as implicit arguments. *) Arguments foo A B c. (* leaves implicit arguments and scopes declared for foo untouched *) Arguments foo A B c : clear implicits (* equivalente too Implicit Arguments foo [] *) Arguments foo A B c : clear scopes (* equivalente too Arguments Scope foo [_ _ _] *) Arguments foo A B c : clear scopes, clear implicits Arguments foo A B c : clear implicits, clear scopes Arguments foo A B c : clear scopes and implicits Arguments foo A B c : clear implicits and scopes (* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *) Arguments foo A B c : default implicits. (* equivalent to Implicit Arguments foo. *) Arguments foo {A B} x , A [B] x. (* equivalent to Implicit Arguments foo [[A] [B]] [B]. *) Arguments foo a !b c !d. (* foo is unfolded by simpl if b and d evaluate to a constructor *) Arguments foo a b c / d. (* foo is unfolded by simpl if applied to 3 arguments *) Arguments foo a !b c / d. (* foo is unfolded by simpl if applied to 3 arguments and if b evaluates to a constructor *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the type infrastructure to handle properly API management of optionsGravatar ppedrot2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14689 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix parsing of :>> and backtrack correctly on the cache of hints for local ↵Gravatar msozeau2011-11-18
| | | | | | contexts git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a printing function to handle single evarsGravatar ppedrot2011-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restore backward compatibility. ":>" declares subinstances in Class ↵Gravatar msozeau2011-11-18
| | | | | | | | | | declarations, in the usual backward mode, the new token ":>>" declares the subinstance as a forward hint. Both declare a coercion in other contexts. Cleanup the code for declarations for less confusion between coercions and subinstance hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
| | | | | | | | | | | how the names of an ltac expression are globalized - allowing the expression to be a constr and in some initial context - and when and how this ltac expression is interpreted - now expecting a pure tactic in a different context). This incidentally found a Ltac bug in Ncring_polynom! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
| | | | | | | | | | | | | | This adds two experimental features to the typeclass implementation: - Path cuts: a way to specify through regular expressions on instance names search pathes that should be avoided (e.g. [proper_flip proper_flip]). Regular expression matching is implemented through naïve derivatives. - Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no longer applied backwards, but introducing a specific [Equivalence] in the environment register a [Reflexive] hint as well. Currently not backwards-compatible, the next patch will allow to specify direction of subclasses hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing beautification of "thm_token" (missing space) + improvements.Gravatar herbelin2011-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For instance, consider this inductive type: Inductive Ind := A | B | C | D. For detecting "match" on this type, one was forced earlier to write code in Ltac using "match goal" and/or "context [...]" and long patterns such as: match _ with A => _ | B => _ | C => _ | D => _ end After this patch, this pattern can be shortened in many alternative ways: match _ with A => _ | _ => _ end match _ with B => _ | _ => _ end match _ in Ind with _ => _ end Indeed, if we want to detect a "match" of a given type, we can either leave at least one branch where a constructor is explicit, or use a "in" annotation. Now, we can also detect any "match" regardless of its type: match _ with _ => _ end Note : this will even detect "match" over empty inductive types. Compatibility should be preserved, since "match _ with end" will continue to correspond only to empty inductive types. Internally, the constr_pattern PCase has changed quite a lot, a few elements are now grouped into a case_info_pattern record, while branches are now lists of given sub-patterns. NB: writing "match" with missing last branches in a constr pattern was actually tolerated by Pattern.pattern_of_glob_constr earlier, since the number of constructor per inductive is unknown there. And this was triggering an uncaught exception in a array_fold_left_2 in Matching later. Oups. At least this patch fixes this issue... Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number of branch in a match pattern. I doubt this was really a problem, but having now linear code instead cannot harm ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
* Applying Tom Prince's patch to support parametric "constructor n" inGravatar herbelin2011-10-25
| | | | | | tactic notations and ltac definitions (see bug report #2496). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14606 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:05:47 +0000