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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/closure.mli')

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