From b63f3d7db6e23746165f2a8501dfc3b52351530b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 17 Feb 2011 16:13:30 +0000
Subject: - Use transparency information all the way through unification and
 conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal
 with respect to evars before rewriting in [rewrite], allowing to see
 instanciations from other subgoals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml  | 3 +++
 kernel/closure.mli | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 6434e14156..8d4758cfd8 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -66,6 +66,9 @@ let with_stats c =
 let all_opaque = (Idpred.empty, Cpred.empty)
 let all_transparent = (Idpred.full, Cpred.full)
 
+let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
+
 module type RedFlagsSig = sig
   type reds
   type red_kind
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 74c91650ac..f4dc5db35a 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -29,6 +29,9 @@ val with_stats: 'a Lazy.t -> 'a
 val all_opaque      : transparent_state
 val all_transparent : transparent_state
 
+val is_transparent_variable : transparent_state -> variable -> bool
+val is_transparent_constant : transparent_state -> constant -> bool
+
 (** Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
-- 
cgit v1.2.3