| Age | Commit message (Collapse) | Author |
|---|
|
Incidentally, this fixes #10056
|
|
The checks were unnecessarily restrictive (since names can be used for
documentation purposes), and the error message was a bit wrong (it
mentioned a restriction on the explicit status of arguments).
|
|
|
|
Removing in passing two Local which are no-ops in practice.
|
|
|
|
output/Arguments.v
output/ArgumentsScope.v
output/Arguments_renaming.v
output/Cases.v
output/Implicit.v
output/PrintInfos.v
output/TranspModType.v
Main changes: monomorphic -> not universe polymorphic, Peano vs Nat
|
|
Of course, this is an under approximation of the expected behavior : unfolding
a constant iff a leaf of its underlying split-tree is reached.
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Implicit arguments can be mentioned anonymously:
Arguments map {_ _} f l.
- To rename implicit arguments, the ": rename" flag must be used:
Arguments map {T1 T2} f l : rename.
Without the ": rename" flag arguments can be used to assert
that a function has indeed the expected number of arguments and
that the arguments are named as expected.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14766 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
