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 /library | |
| 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 'library')
| -rw-r--r-- | library/impargs.ml | 4 | ||||
| -rw-r--r-- | library/impargs.mli | 2 |
2 files changed, 6 insertions, 0 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 2d5ffe9ab0..5d689faa0b 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -246,6 +246,10 @@ let compute_auto_implicits env flags enriching t = if enriching then compute_implicits_flags env flags true t else compute_implicits_gen false false false true true env t +let compute_implicits_names env t = + let _, impls = compute_implicits_gen false false false false true env t in + List.map fst impls + (* Extra information about implicit arguments *) type maximal_insertion = bool (* true = maximal contextual insertion *) diff --git a/library/impargs.mli b/library/impargs.mli index 6315745911..04251f332e 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -95,6 +95,8 @@ type manual_implicits = manual_explicitation list val compute_implicits_with_manual : env -> types -> bool -> manual_implicits -> implicit_status list +val compute_implicits_names : env -> types -> name list + (** {6 Computation of implicits (done using the global environment). } *) val declare_var_implicits : variable -> unit |