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 /interp | |
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 'interp')
-rw-r--r-- | interp/constrintern.ml | 13 | ||||
-rw-r--r-- | interp/constrintern.mli | 4 |
2 files changed, 14 insertions, 3 deletions
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 |