- 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/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