From c4d62e3686926c27b172636ca8b746814d13a462 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 23:34:07 +0100
Subject: Moving type_uconstr to Pretyping.

---
 intf/tacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index b1dc174d4b..0aa3b936ca 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -122,7 +122,7 @@ type open_glob_constr = unit * glob_constr_and_expr
 type binding_bound_vars = Id.Set.t
 type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern
 
-type 'a delayed_open =
+type 'a delayed_open = 'a Pretyping.delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
 type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
-- 
cgit v1.2.3