aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Collapse)AuthorAge
...
* Pattern as a mli-only file, operations in PatternopsGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
| | | | | | Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tacexpr as a mli-only, the few functions there are now in TacopsGravatar letouzey2012-05-29
| | | | | | | NB: former Tacexpr.no_move is now Tacexpr.MoveLast (when introducing, intro with no move is intro as last) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
| | | | | | Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tactic unfold always asks for comma between names.Gravatar pboutill2012-05-09
| | | | | | Else the parser takes "at" as a constant to unfold in "unfold plus at ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15290 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of r15148 in order to compile with Camlp4Gravatar pboutill2012-04-27
| | | | | | + comment correction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15253 85f007b7-540e-0410-9357-904b9bb8a0f7
* migrate g_obligations.ml4 in parsingGravatar letouzey2012-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Program: avoid staying in program mode after a failed Program commandGravatar letouzey2012-04-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15247 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
| | | | | | | | | | | | | | | | constr as argument (rather than openconstr) assumed that the evar_map output by pretyping was irrelevant as the final constr didn't have any evars. However, if said constr was defined using pre-existing evars from the context, the evars may be instantiated by pretyping, hence dropping the output evar_map led to inconsistent proof terms. This fixes bug #2739 ( https://coq.inria.fr/bugs/show_bug.cgi?id=2739 ). Thanks Arthur for noticing it. Note: change still has the bug, because more serious issues interfered with my fix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed syntax BeginSubproof/EndSubproof. It has been replaced byGravatar aspiwack2012-04-13
| | | | | | | | braces ( { / } ). BeginSuproof n (where n is a goal number) can be replaced by Focus n. { . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
| | | | | | Signed-off-by: Edward Z. Yang <ezyang@mit.edu> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15148 85f007b7-540e-0410-9357-904b9bb8a0f7
* "A -> B" is a notation for "forall _ : A, B".Gravatar pboutill2012-04-12
| | | | | | | No good reason for that except uniformity so revert this commit if you find a reason against it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
| | | | | | | | | | | | | | | | | | | | | | | | - fixing missing spaces in the format of the exists' notations (Logic.v); - fixing wrong variable name in check_is_hole error message (topconstr.ml); - interpret expressions with open binders such as "forall x y, t" as "forall (x:_) (y:_),t" instead of "forall (x y:_),t" to avoid the "implicit type" of a variable being propagated to the type of another variable of different base name. An open question remains: when writing explicitly "forall (x y:_),t", should the types of x and y be the same or not. To avoid the "bug" that x and y have implicit types but the one of x takes precedences, I enforced the interpretation (in constrintern, not in parsing) that "forall (x y:_),t" means the same as "forall (x:_) (y:_),t". However, another choice could have been made. Then one would have to check that if x and y have implicit types, they are the same; also, glob_constr should ideally be changed to support a GProd and GLam with multiple names in the same type, especially if this type is an evar. On the contrary, one might also want e.g. "forall x y : list _, t" to mean "forall (x:list _) (y:list _), t" with distinct instanciations of "_" ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in a message.Gravatar aspiwack2012-03-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15105 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a command "Unfocused" which returns an error when the proof isGravatar aspiwack2012-03-30
| | | | | | not fully unfocused (in the style of the Guarded command). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 85f007b7-540e-0410-9357-904b9bb8a0f7
* info_trivial, info_auto, info_eauto, and debug (trivial|auto)Gravatar letouzey2012-03-30
| | | | | | | | | | | | | | | | | | | | | | | To mitigate the lack of a general "info" tactical, let's introduce some specialized tactics info_trivial, info_auto and info_eauto that display the basic tactics used when solving a goal. We also add tactics "debug trivial" and "debug auto" which display every basic tactics attempted by trivial or auto. Triggering the "info" or "debug" mode for auto, eauto, trivial can also be done now via global options, such as Set Debug Auto or Set Info Eauto. In case both debug and info modes are activated, the debug mode takes precedence. NB: it would be nice to name these tactics "info xxx" instead of "info_xxx", but I don't see how to implement a "info eauto" in eauto.ml4 (hence by TACTIC EXTEND) while keeping a generic "info foo" tactic in g_ltac.ml4 (useful to display a nice message about the unavailability of the general info). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
| | | | | | No grammar entries for these tactics since coq 8.0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight change in the semantics of arguments scopes: scopes can noGravatar herbelin2012-03-26
| | | | | | | | | | | longer be bound to Funclass or Sortclass (this does not seem to be useful). [An exception is when using modules, if a constant foo is expanded into a type, a "Bind Scope sc with foo" starts binding Sortclass]. Also reworked reference manual for Arguments Scopes and Bind Scopes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15098 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove undocumented command "Delete foo"Gravatar letouzey2012-03-23
| | | | | | | | | This command isn't trivial to port to the forthcoming evolution of backtracking in coqtop. Moreover, it isn't clear whether this "Delete" works well in advanced situation (was not updating frozen states). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15084 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
| | | | | | | There're not compatible with the current Backtrack mecanism used both by ProofGeneral and CoqIDE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ppvernac: nicer printing of proof delimiters { ... }Gravatar letouzey2012-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15076 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2724 (using notations with binders in cases patternsGravatar herbelin2012-03-20
| | | | | | was provoking an anomaly instead of a regular error). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15070 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The optimisation done of Namegen.visibly_occur_id did not preserve the previous behavior when pr_constr/constr_extern/detype were called on a term with free rel variables. We backtrack on it to go back to the 8.2 behavior. Seized this opportunity to clarify the meaning of the at_top flag in constrextern.ml and printer.ml and to rename it into goal_concl_style. The badly-named at_top flag was introduced in Coq 6.3 in 1999 to mean that when printing variables bound in the goal, names had to avoid the names of the variables of the goal context, so as to keep naming stable when using "intro"; in r4458, printing improved by not avoiding names that were short names of global definitions, e.g. "S", or "O" (except when the at_top flag was on for compatibility reasons). Other printing strategies could be possible in the non-goal-concl-style mode. For instance, all bound variables could be made distinct in a given expression, even if no clash occur, therefore following so-called Barendregt's convention. This could be done by setting "avoid" to "ids_of_rel_context (rel_context env)" in extern_constr and extern_type (and then, Namegen.visibly_occur_id could be re-simplified again!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicGravatar herbelin2012-03-20
| | | | | | | | | | | | tactic arguments of ltac functions). Added support for recursive entries in ARGUMENT EXTEND, for right-hand sides of ARGUMENT EXTEND raising exceptions and for right-hand sides referring to "loc". Also fixed parsing level of initial value in create_arg (raw instead of glob). Thanks to the Ssreflect plugin for revealing these problems. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15065 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 00:37:49 +0000