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

11 files changed, 37 insertions, 19 deletions

diff --git a/CHANGES b/CHANGES
index 364df5b9c..47f131ce9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -435,6 +435,10 @@ Tools
 - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
 - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
 - The binary "parser" has been renamed to "coq-parser".
+- Improved coqdoc and dump of globalization information to give more meta-information
+  on identifiers. All categories of Coq definitions are supported, which makes
+  typesetting trivial in the generated documentation. Support for hyperlinking
+  and indexing developments in the tex output has been implemented as well.
 
 Miscellaneous
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 79ef00972..027aae7a7 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -168,7 +168,7 @@ let build_newrecursive
 	  if Impargs.is_implicit_args()
 	  then Impargs.compute_implicits  env0 arity
 	  else [] in
-	let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in
+	let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
         (Environ.push_named (recname,None,arity) env, impls'))
       (env0,[]) lnameargsardef in
   let recdef =
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 503f34619..191400212 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 *)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index be7c75663..15c816b5b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -26,8 +26,10 @@ open Inductiveops
 
 (* To interpret implicits and arg scopes of recursive variables in
    inductive types and recursive definitions *)
+type var_internalisation_type = Inductive | Recursive | Method
+
 type var_internalisation_data =
-    identifier list * Impargs.implicits_list * scope_name option list
+  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
 
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
@@ -279,13 +281,20 @@ let rec it_mkRLambda env body =
    [vars2] is the set of global variables, env is the set of variables
    abstracted until this point *)
 
+let string_of_ty = function
+  | Inductive -> "ind"
+  | Recursive -> "def"
+  | Method -> "meth"
+
 let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let l,impl,argsc = List.assoc id impls in
+    let ty, l,impl,argsc = List.assoc id impls in
     let l = List.map 
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
+    let tys = string_of_ty ty in
+      Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
     RVar (loc,id), impl, argsc, l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 27a46daf1..9169e5fbf 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -39,8 +39,10 @@ open Pretyping
    argument associates a list of implicit positions and scopes to
    identifiers declared in the [rel_context] of [env] *)
 
+type var_internalisation_type = Inductive | Recursive | Method 
+    
 type var_internalisation_data =
-    identifier list * Impargs.implicits_list * scope_name option list
+  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
 
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index c1d7f34ce..7c7362cad 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -284,7 +284,7 @@ Definition predicate_implication {l : list Type} :=
 (** Notations for pointwise equivalence and implication of predicates. *)
 
 Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope.
-Infix "-∙>" := predicate_implication (at level 70) : predicate_scope.
+Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope.
 
 Open Local Scope predicate_scope.
 
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 11f710997..d299d9dda 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Program.Equality"); compile-command: "make -C ../.. TIME='time'" -*- *)
+(* -*- coq-prog-name: "~/research/coq/trunk/bin/coqtop.byte"; coq-prog-args: ("-emacs-U"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -498,12 +498,13 @@ Ltac equations := set_eos ;
     | _ => nonrec_equations
   end.
 
+(*
 Equations NoConfusion_nat (P : Prop) (x y : nat) : Prop :=
 NoConfusion_nat P 0 0 := P -> P ;
 NoConfusion_nat P 0 (S y) := P ;
 NoConfusion_nat P (S x) 0 := P ;
 NoConfusion_nat P (S x) (S y) := (x = y -> P) -> P.
-Debug Off.
+
   Solve Obligations using equations.
 
 Equations noConfusion_nat (P : Prop) (x y : nat) (H : x = y) : NoConfusion_nat P x y :=
@@ -569,3 +570,4 @@ noConfusion_list P A (cons a x) (cons a x) refl := λ p : a = a -> x = x -> P, p
 Instance list_noconf A : NoConfusionPackage (list A) :=
   NoConfusion := λ P, Π x y, x = y -> NoConfusion_list P A x y ;
   noConfusion := λ P x y, noConfusion_list P A x y.
+*)
\ No newline at end of file
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