diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-11 18:28:41 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-11 18:28:41 +0000 |
| commit | 5953161cd65194e341b2f8255501e7a15de498ac (patch) | |
| tree | 6e3baa7b3ac9f85d82399dc4fb62f121b3f695ec /toplevel/record.ml | |
| 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 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index b1271f516..ae97a8db4 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -38,7 +38,7 @@ let interp_evars evdref env ?(impls=([],[])) k typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (out_name na, ([], impl, Notation.compute_arguments_scope typ)) + in (out_name na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env l = List.fold_left |