summaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /interp/constrintern.mli
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'interp/constrintern.mli')
-rw-r--r--interp/constrintern.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index acb13a8b..02a51e7e 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: constrintern.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: constrintern.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
(*i*)
open Names
@@ -53,7 +53,7 @@ type var_internalization_data =
identifier list *
(* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
- Impargs.implicits_list * (* signature of impargs of the variable *)
+ Impargs.implicit_status list * (** signature of impargs of the variable *)
scope_name option list (* subscopes of the args of the variable *)
(* A map of free variables to their implicit arguments and scopes *)