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
---
 checker/closure.ml  | 3 +++
 checker/closure.mli | 3 +++
 2 files changed, 6 insertions(+)

(limited to 'checker')

diff --git a/checker/closure.ml b/checker/closure.ml
index 8cf8c4c071..bd73471341 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -52,6 +52,9 @@ type transparent_state = Idpred.t * Cpred.t
 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/checker/closure.mli b/checker/closure.mli
index a1a23c6cb5..8556f26afa 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -30,6 +30,9 @@ type transparent_state = Idpred.t * Cpred.t
 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