From ba0975d00f49684e33f763e171f9578a702eec85 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Sep 2016 16:51:19 +0200
Subject: Move glob_constr_ltac_closure to evar_refiner.

---
 pretyping/pretyping.ml  | 1 -
 pretyping/pretyping.mli | 1 -
 2 files changed, 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b4d87dfdb0..3fae20bcb9 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -47,7 +47,6 @@ open Misctypes
 module NamedDecl = Context.Named.Declaration
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
-type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * EConstr.constr
 
 (************************************************************************)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 6e533f1784..1bde4b44ce 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,7 +27,6 @@ val search_guard :
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
 
-type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
 type inference_hook = env -> evar_map -> evar -> evar_map * constr
-- 
cgit v1.2.3