diff options
| author | pboutill | 2011-02-10 14:11:01 +0000 |
|---|---|---|
| committer | pboutill | 2011-02-10 14:11:01 +0000 |
| commit | 6df4e0fe6bc6076bc95a1a71d28ae049d04ba517 (patch) | |
| tree | 6e749cf9e23637a28185daac6fb2e12a3d0d6ab4 /interp/constrintern.mli | |
| parent | 533c5085e4f9ce392a87841ab67e45c557aa769e (diff) | |
Data structure telling implicits of local variables is a map in the
intern_env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 12dc6be165..2cb7065895 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -40,6 +40,7 @@ type var_internalization_type = | Inductive of identifier list (* list of params *) | Recursive | Method + | Definition type var_internalization_data = var_internalization_type * @@ -52,8 +53,7 @@ type var_internalization_data = scope_name option list (** subscopes of the args of the variable *) (** A map of free variables to their implicit arguments and scopes *) -type internalization_env = - (identifier * var_internalization_data) list +type internalization_env = var_internalization_data Idmap.t val empty_internalization_env : internalization_env |