From cf95f2a791c263c7aaa3b488d1b09eaafc29be2b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Jun 2016 16:30:32 +0200
Subject: closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs
 module)

 For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
---
 pretyping/unification.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/unification.ml')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c17879739a..0c1ce0d2f8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -460,7 +460,7 @@ let use_metas_pattern_unification flags nb l =
      Array.for_all (fun c -> isRel c && destRel c <= nb) l
 
 type key = 
-  | IsKey of Closure.table_key
+  | IsKey of CClosure.table_key
   | IsProj of projection * constr
 
 let expand_table_key env = function
@@ -1210,8 +1210,8 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
 
 let is_mimick_head ts f =
   match kind_of_term f with
-  | Const (c,u) -> not (Closure.is_transparent_constant ts c)
-  | Var id -> not (Closure.is_transparent_variable ts id)
+  | Const (c,u) -> not (CClosure.is_transparent_constant ts c)
+  | Var id -> not (CClosure.is_transparent_variable ts id)
   | (Rel _|Construct _|Ind _) -> true
   | _ -> false
 
-- 
cgit v1.2.3