aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Collapse)AuthorAge
* Fixing printing of @f with no argumentsGravatar herbelin2012-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Constrextern is allow to use partially applied notationsGravatar pboutill2012-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
| | | | | | | | | | | | | | | | | | First Notations, syntactic definitions, primitive entries are tackled to build raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns are internalized as cases_pattern or applied inductive (dealing with implicit args, or_pattern refactoring, aliases). It is more uniform, it allows notations for non fully applied constructors but : - It does not raise a warning when an identifier is also a global_reference different than a constructor. - It looks for implicit arguments twice. (because finding scopes of arguments asks for implicit arguments). - It does not deal anymore with constants that evaluates to constructor. (This one is voluntary, dealing with implicit & notations is already a hell full of bugs so what will be next step ? Any terms that computes to a pattern ???) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing some str with strbrkGravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15389 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more Univ in grammar.cmaGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
* global_reference migrated from Libnames to new Globnames, less deps in ↵Gravatar letouzey2012-05-29
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
* slim down a bit genarg.ml (pr_intro_pattern forgotten there)Gravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15380 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* 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
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
| | | | | | Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Impossible branches inference fixup (bug 2761)Gravatar pboutill2012-05-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 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 the "capture" check newly introduced in r15122 whenGravatar herbelin2012-04-07
| | | | | | | | | | internalizing declaration of contexts of the form "(x y : P x)": - don't forget to catch the error in intern_context; - check capture on glob_constr rather than constr_expr so that binders possibly introduced by notations are recognized as such; - give a more expressive error message. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15123 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unifying the different procedures for interning binders.Gravatar herbelin2012-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15122 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
* 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
* Fixing deactivation of scope at printing time in the body of aGravatar herbelin2012-03-26
| | | | | | | lam or prod to be consistent with what is done at parsing time (see coq-club on 25/3/2012). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15093 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
* 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
* Second step of integration of Program:Gravatar msozeau2012-03-14
| | | | | | | | - Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 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
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
| | | | | | | | This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf. An other wrong externalize function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 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
* Fix compilation of Constrintern...Gravatar pboutill2012-02-29
| | | | | | I love being push under presure to commit and do not try my fixup ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15003 85f007b7-540e-0410-9357-904b9bb8a0f7
* RefMan update about match syntax.Gravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the syntax of pattern matching, the arguments of the inductive in the "in"Gravatar pboutill2012-02-29
| | | | | | | | clause can be any pattern. It is expanded as a match in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15001 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
* Debugger vs tracer: Two different behaviors wrt printing: The debuggerGravatar herbelin2012-02-01
| | | | | | | | | runs in separate process. It has no access to the global env and it should not request it. The tracer runs in the same process as Coq and has full access to the global env and to regular pretty-printing of global names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
* Printing bugs with match patterns:Gravatar herbelin2012-01-27
| | | | | | | | | | | - namegen.ml: if a matching variable has the same name as a constructor, rename it, even if the conflicting constructor name is defined in a different module; - constrextern.ml: protect code for printing cases as terms are from requesting info in the global env when printers are called from ocamldebug since the global env is undefined in this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added documentation for "Set Parsing Explicit" + fixed mistakenlyGravatar herbelin2012-01-20
| | | | | | committed "assert" in commit r14928. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added new command "Set Parsing Explicit" for deactivating parsing (andGravatar herbelin2012-01-20
| | | | | | printing) of implicit arguments (a priori useful for teaching). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
| | | | | | | which do not necessarily depend on their parameter (e.g. a notation for "fun x => t" might match also "fun _ => t"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14926 85f007b7-540e-0410-9357-904b9bb8a0f7
* Boolean Option Patterns CompatibilityGravatar pboutill2012-01-19
| | | | | | | switch between "all arguments no parameters" and "explicit params and args" for constructor arguments in patterns. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parameters in pattern first step.Gravatar pboutill2012-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In interp/constrintern.ml, '_' for constructor parameter are required if you use AppExpl ('@Constr') and added in order to be erased at the last time if you do not use '@'. It makes the use of notation in pattern more permissive. For example, -8<------ Inductive I (A: Type) : Type := C : A -> I A. Notation "x <: T" := (C T x) (at level 38). Definition uncast A (x : I A) := match x with | x <: _ => x end. -8<------ was forbidden. Backward compatibility is strictly preserved expect for syntactic definitions: While defining "Notation SOME = @Some", SOME had a special treatment and used to be an alias of Some in pattern. It is now uniformly an alias of @Some ('_' must be provided for parameters). In interp/constrextern.ml, except if all the parameters are implicit and all the arguments explicit (This covers all the cases of the test-suite), pattern are generated with AppExpl (id est '@') (so with '_' for parameters) in order to become compatible in any case with future behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14909 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtracking on r14876 (fix for bug #2267): extra scopes might beGravatar herbelin2012-01-05
| | | | | | | useful in the presence of coercions to Funclass. Fixed the bug differently. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14880 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Arguments Scope bug when too many scopes are given (bug #2667).Gravatar herbelin2012-01-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14876 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2634 (unscoped notations were disturbing theGravatar herbelin2011-12-18
| | | | | | interpretation order of scoped notations). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14819 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
* Fixing amazing loop when using eta-expansion in pattern-matching forGravatar herbelin2011-12-16
| | | | | | | | printing notations. Since notation printing is not typed, printing "F G" using a notation for "f (fun x => g)" recursively eta-expands G, then x, then a new x and so on forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-11 11:40:20 +0000