aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.mli')
-rw-r--r--interp/constrextern.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b5242b347..ffa891c50 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -9,6 +9,7 @@
open Names
open Term
open Termops
+open EConstr
open Environ
open Libnames
open Globnames
@@ -41,7 +42,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> sorts -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
- Context.Rel.t -> local_binder_expr list
+ rel_context -> local_binder_expr list
(** Printing options *)
val print_implicits : bool ref