Proofview.Goal primitive now return EConstrs.

7 files changed, 11 insertions, 4 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 4d2859fb0..93bd88fe4 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -221,6 +221,7 @@ module Btauto = struct
     Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
+      let concl = EConstr.Unsafe.to_constr concl in
       let t = decomp_term (Tacmach.New.project gl) concl in
       match t with
       | Term.App (c, [|typ; p; _|]) when c === eq ->
@@ -235,6 +236,7 @@ module Btauto = struct
   let tac =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
+      let concl = EConstr.Unsafe.to_constr concl in
       let sigma = Tacmach.New.project gl in
       let eq = Lazy.force eq in
       let bool = Lazy.force Bool.typ in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6295e004e..130f01e97 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -230,7 +230,7 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype (cstr:pconstructor) special default gls=
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) default in
   let body = EConstr.Unsafe.to_constr body in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
@@ -321,6 +321,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	 let special=mkRel (1+nargs-argind) in
 	 refresh_universes (type_of ti) (fun intype ->
          refresh_universes (type_of default) (fun outtype ->
+         let default = EConstr.of_constr default in
          let proj =
            Tacmach.New.of_old (build_projection intype cstr special default) gl
          in
@@ -388,6 +389,7 @@ let discriminate_tac (cstr,u as cstru) p =
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
     let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
     let proj = Tacmach.New.of_old (build_projection intype cstru trivial concl) gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let injt=app_global _f_equal
 			[|intype;outtype;proj;t1;t2;mkVar hid|] in
     let endt k =
@@ -498,6 +500,7 @@ let mk_eq f c1 c2 k =
 let f_equal =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let cut_eq c1 c2 =
       try (* type_of can raise an exception *)
         Tacticals.New.tclTHENS
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e73166be2..c3254010a 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -41,7 +41,7 @@ let clear ids { it = goal; sigma } =
   let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
   let env = Goal.V82.env sigma goal in
   let sign = Goal.V82.hyps sigma goal in
-  let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in
+  let cl = Goal.V82.concl sigma goal in
   let evdref = ref (Evd.clear_metas sigma) in
   let (hyps, concl) =
     try Evarutil.clear_hyps_in_evi env evdref sign cl ids
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index f9802ee5e..bffca6223 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -470,7 +470,7 @@ let rec fourier () =
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
-    let goal = Termops.strip_outer_cast sigma (EConstr.of_constr concl) in
+    let goal = Termops.strip_outer_cast sigma concl in
     let goal = EConstr.Unsafe.to_constr goal in
     let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index f39549514..72290e681 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1857,6 +1857,7 @@ let destructure_goal =
 	  in
 	  Tacticals.New.tclTHEN goal_tac destructure_hyps
     in
+    let concl = EConstr.Unsafe.to_constr concl in
     (loop concl)
   end }
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 04a747fb4..5f8a0b2d5 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -452,6 +452,7 @@ let quote f lid =
     let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
     let ivs = compute_ivs f cl gl in
     let concl = Proofview.Goal.concl gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let quoted_terms = quote_terms ivs [concl] in
     let (p, vm) = match quoted_terms with
       | [p], vm -> (p,vm)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index aa91494eb..d34c9325e 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1078,7 +1078,7 @@ END
 let thin id sigma goal =
   let ids = Id.Set.singleton id in
   let env = Goal.V82.env sigma goal in
-  let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in
+  let cl = Goal.V82.concl sigma goal in
   let evdref = ref (Evd.clear_metas sigma) in
   let ans =
     try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids)