From 5953161cd65194e341b2f8255501e7a15de498ac Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 11 Sep 2008 18:28:41 +0000
Subject: 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
---
 interp/constrintern.ml  | 13 +++++++++++--
 interp/constrintern.mli |  4 +++-
 2 files changed, 14 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index be7c75663b..15c816b5b4 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 27a46daf19..9169e5fbf1 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
-- 
cgit v1.2.3