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 /toplevel/command.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/command.ml')
| -rw-r--r-- | toplevel/command.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index f18cecb207..9ae3f8e826 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -442,7 +442,7 @@ let declare_eliminations sp = (* 3b| Mutual inductive definitions *) -let compute_interning_datas env l nal typl impll = +let compute_interning_datas env ty l nal typl impll = let mk_interning_data na typ impls = let idl, impl = let impl = @@ -452,7 +452,7 @@ let compute_interning_datas env l nal typl impll = let sub_impl' = List.filter is_status_implicit sub_impl in (List.map name_of_implicit sub_impl', impl) in - (na, (idl, impl, compute_arguments_scope typ)) in + (na, (ty, idl, impl, compute_arguments_scope typ)) in (l, list_map3 mk_interning_data nal typl impll) let declare_interning_data (_,impls) (df,c,scope) = @@ -526,7 +526,7 @@ let interp_mutual paramsl indl notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun _ -> userimpls) fullarities in - let impls = compute_interning_datas env0 params indnames fullarities indimpls in + let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -832,7 +832,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = compute_interning_datas env 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 *) |