diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 11:49:20 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-15 11:49:20 +0000 |
| commit | e0d81e2e0f4051c1bcf25b923cef4699cd48c535 (patch) | |
| tree | ddea3f34f499e59287c0008743ecd2cf275311ba /contrib | |
| parent | 6bfc052779929474cc18bf08da1c88319dddbffb (diff) | |
Do a second pass on the treatment of user-given implicit arguments. Now
works in inductive type definitions and fixpoints. The semantics of
an implicit inductive parameter is maybe a bit weird: it is implicit in the
inductive definition of constructors and the contructor types but not in
the inductive type itself (ie. to model the fact that one rarely wants A
in vector A n to be implicit but in vnil yes). Example in test-suite/
Also, correct the handling of the implicit arguments across sections.
Every definition which had no explicitely given implicit arguments was
treated as if we asked to do global automatic implicit arguments on
section closing. Hence some arguments were given implicit status for no
apparent reason.
Also correct and test the parsing rule which disambiguates between {wf
..} and {A ..}.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10677 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index b06880bd3..9c40c861e 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -374,7 +374,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let impls = Command.compute_interning_datas env [] fixnames fixtypes in + let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) |