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

4 files changed, 12 insertions, 11 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 8dcbf4b28..bf9ee1269 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -99,7 +99,7 @@ let interp_type_evars evdref env ?(impls=([],[])) typ =
 
 let mk_interning_data env na impls typ =
   let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
-  in (na, ([], impl, Notation.compute_arguments_scope typ))
+  in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
     
 let interp_fields_evars isevars env avoid l =
   List.fold_left
@@ -160,8 +160,8 @@ let new_class id par ar sup props =
   let supnames = 
     List.fold_left (fun acc b -> 
       match b with
-	  LocalRawAssum (nl, _, _) -> nl @ acc
-	| LocalRawDef _ -> assert(false))
+      | LocalRawAssum (nl, _, _) -> nl @ acc
+      | LocalRawDef _ -> assert(false))
       [] sup
   in
 
@@ -241,7 +241,7 @@ let new_class id par ar sup props =
 	      params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
 	    in
 	      IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y)
-			     fields (Recordops.lookup_projections (kn,0)))
+				 (List.rev fields) (Recordops.lookup_projections (kn,0)))
   in
   let ctx_context =
     List.map (fun ((na, b, t) as d) -> 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index f18cecb20..9ae3f8e82 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 *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 227152f14..a1e976c79 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -56,10 +56,11 @@ val declare_assumption : identifier located list ->
 val declare_interning_data : 'a * Constrintern.implicits_env ->
     string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
 
-val compute_interning_datas :  Environ.env -> 'a list -> 'b list ->
+val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> 
+  'a list -> 'b list ->
   Term.types list ->Impargs.manual_explicitation list list ->
   'a list *
-    ('b * (Names.identifier list * Impargs.implicits_list *
+    ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list *
 	      Topconstr.scope_name option list))
     list
 
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