Add primitives in Goal.V82 to access the goal in nf_evar'd form.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17025 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 28 insertions, 0 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index a9a0be28d..ebd6ca84d 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -490,16 +490,32 @@ module V82 = struct
     let evi = content evars gl in
     Evd.evar_filtered_env evi
 
+  (* same as [env], but ensures that existential variables are
+     normalised *)
+  let nf_env evars gl =
+    Evarutil.nf_env_evar evars (env evars gl)
+
   (* Old style hyps primitive *)
   let hyps evars gl =
     let evi = content evars gl in
     Evd.evar_filtered_hyps evi
 
+  (* same as [hyps], but ensures that existential variables are
+     normalised. *)
+  let nf_hyps evars gl =
+    let hyps = Environ.named_context_of_val (hyps evars gl) in
+    Environ.val_of_named_context (Evarutil.nf_named_context_evar evars hyps)
+
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = content evars gl in
     evi.Evd.evar_concl
 
+  (* same as [concl] but ensures that existential variables are
+     normalised. *)
+  let nf_concl evars gl =
+    Evarutil.nf_evar evars (concl evars gl)
+
   (* Access to ".evar_extra" *)
   let extra evars gl =
     let evi = content evars gl in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 39c7ed793..1f04ce8c1 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -178,12 +178,24 @@ module V82 : sig
   (* Old style env primitive *)
   val env : Evd.evar_map -> goal -> Environ.env
 
+  (* same as [env], but ensures that existential variables are
+     normalised *)
+  val nf_env : Evd.evar_map -> goal -> Environ.env
+
   (* Old style hyps primitive *)
   val hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
+  (* same as [hyps], but ensures that existential variables are
+     normalised. *)
+  val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
+
   (* Access to ".evar_concl" *)
   val concl : Evd.evar_map -> goal -> Term.constr
 
+  (* same as [concl] but ensures that existential variables are
+     normalised. *)
+  val nf_concl : Evd.evar_map -> goal -> Term.constr
+
   (* Access to ".evar_extra" *)
   val extra : Evd.evar_map -> goal -> Evd.Store.t