A version of convert_concl and convert_hyp in new proof engine.

Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).

4 files changed, 12 insertions, 5 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5de7b901d3..2d302510eb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -492,18 +492,18 @@ and mk_casegoals sigma goal goalacc p c =
   (acc'',lbrty,conclty,sigma,p',c')
 
 
-let convert_hyp sign sigma (id,b,bt as d) =
+let convert_hyp check sign sigma (id,b,bt as d) =
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
     apply_to_hyp sign id
       (fun _ (_,c,ct) _ ->
         let env = Global.env_of_context sign in
-        if !check && not (is_conv env sigma bt ct) then
+        if check && not (is_conv env sigma bt ct) then
 	  error ("Incorrect change of the type of "^(Id.to_string id)^".");
-        if !check && not (Option.equal (is_conv env sigma) b c) then
+        if check && not (Option.equal (is_conv env sigma) b c) then
 	  error ("Incorrect change of the body of "^(Id.to_string id)^".");
-       if !check then reorder := check_decl_position env sign d;
+       if check then reorder := check_decl_position env sign d;
        d) in
   reorder_val_context env sign' !reorder
 
@@ -665,7 +665,7 @@ let prim_refiner r sigma goal =
           ([sg], sigma)
 
     | Convert_hyp (id,copt,ty) ->
-	let (gl,ev,sigma) = mk_goal (convert_hyp sign sigma (id,copt,ty)) cl in
+	let (gl,ev,sigma) = mk_goal (convert_hyp !check sign sigma (id,copt,ty)) cl in
 	let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
 	([gl], sigma)
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index da54ef0a86..7714b86584 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -51,3 +51,6 @@ type refiner_error =
 exception RefinerError of refiner_error
 
 val catchable_exception : exn -> bool
+
+val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
+  Context.named_declaration -> Environ.named_context_val
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9f8458ba79..8fe924e0fd 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -877,6 +877,8 @@ module Goal = struct
   let hyps { env=env } = Environ.named_context env
   let concl { concl=concl } = concl
 
+  let raw_concl { concl=concl } = concl
+
   let nf_enter_t = Goal.nf_enter begin fun env sigma concl self ->
     {env=env;sigma=sigma;concl=concl;self=self}
   end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 0eae9b6056..ebaa632679 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -403,6 +403,8 @@ module Goal : sig
   val env : 'a t -> Environ.env
   val sigma : 'a t -> Evd.evar_map
 
+  val raw_concl : 'a t -> Term.constr
+
   (* [nf_enter t] execute the goal-dependent tactic [t] in each goal
      independently. In particular [t] need not backtrack the same way in
      each goal. *)