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

0 files changed, 0 insertions, 0 deletions