diff options
| author | msozeau | 2008-09-11 18:28:41 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-11 18:28:41 +0000 |
| commit | 5953161cd65194e341b2f8255501e7a15de498ac (patch) | |
| tree | 6e3baa7b3ac9f85d82399dc4fb62f121b3f695ec /contrib/subtac | |
| parent | cb18488b07fb6f9ba3e6e7ac854bbe68aa630e39 (diff) | |
Add enough information to correctly globalize recursive calls in inductive and
recursive definitions and references to previous fields in record and
classes definitions. Fixes the corresponding typesetting issue in coqdoc
output.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac')
| -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 503f346193..1914002124 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -385,7 +385,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 fiximps in + let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) |