aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-11 18:28:41 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-09-11 18:28:41 +0000
commit5953161cd65194e341b2f8255501e7a15de498ac (patch)
tree6e3baa7b3ac9f85d82399dc4fb62f121b3f695ec /interp/constrintern.mli
parentcb18488b07fb6f9ba3e6e7ac854bbe68aa630e39 (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/constrintern.mli')
-rw-r--r--interp/constrintern.mli4
1 files changed, 3 insertions, 1 deletions
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