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 +++ 1 file changed, 3 insertions(+) (limited to 'kernel/closure.ml') diff --git a/kernel/closure.ml b/kernel/closure.ml index 6434e1415..8d4758cfd 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 -- cgit v1.2.3