- 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

2 files changed, 6 insertions, 0 deletions

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
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 74c91650a..f4dc5db35 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