diff options
| author | gareuselesinge | 2011-11-21 17:03:46 +0000 |
|---|---|---|
| committer | gareuselesinge | 2011-11-21 17:03:46 +0000 |
| commit | 41744ad1706fc5f765430c63981bf437345ba9fe (patch) | |
| tree | 2ae0e746c5156109e8d98e6a13aba149104ce3c6 /toplevel/vernacexpr.ml | |
| parent | b1bfd9757d33d36b9fc009a97173ea7db2d5196d (diff) | |
New Arguments vernacular
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
Diffstat (limited to 'toplevel/vernacexpr.ml')
| -rw-r--r-- | toplevel/vernacexpr.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index bae6cfcdd9..575735230d 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -224,8 +224,6 @@ type vernac_expr = | VernacOpenCloseScope of (locality_flag * bool * scope_name) | VernacDelimiters of scope_name * string | VernacBindScope of scope_name * class_rawexpr list - | VernacArgumentsScope of locality_flag * reference or_by_notation * - scope_name option list | VernacInfix of locality_flag * (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of @@ -318,6 +316,12 @@ type vernac_expr = locality_flag * onlyparsing_flag | VernacDeclareImplicits of locality_flag * reference or_by_notation * (explicitation * bool * bool) list list + | VernacArguments of locality_flag * reference or_by_notation * + ((name * bool * (loc * string) option * bool * bool) list) list * + int * [ `SimplDontExposeCase | `SimplNeverUnfold + | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list + | VernacArgumentsScope of locality_flag * reference or_by_notation * + scope_name option list | VernacReserve of simple_binder list | VernacGeneralizable of locality_flag * (lident list) option | VernacSetOpacity of |