Proofview.Goal primitive now return EConstrs.

5 files changed, 8 insertions, 15 deletions

diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d53248a049..188d041c14 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -355,7 +355,7 @@ let refine_tac ist simple c =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags = constr_flags in
-    let expected_type = Pretyping.OfType (EConstr.of_constr concl) in
+    let expected_type = Pretyping.OfType concl in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma ->
       let Sigma (c, sigma, p) = c.delayed env sigma in
@@ -647,7 +647,6 @@ let hResolve id c occ t =
   let sigma = Sigma.to_evar_map sigma in
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
-  let concl = EConstr.of_constr concl in
   let env_ids = Termops.ids_of_context env in
   let c_raw = Detyping.detype true env_ids env sigma c in
   let t_raw = Detyping.detype true env_ids env sigma t in
@@ -694,6 +693,7 @@ let hget_evar n =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let sigma = Tacmach.New.project gl in
   let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.Unsafe.to_constr concl in
   let evl = evar_list concl in
   let concl = EConstr.of_constr concl in
   if List.length evl < n then
@@ -748,7 +748,6 @@ let  mkCaseEq a  : unit Proofview.tactic =
          [Tactics.generalize [(mkApp(EConstr.of_constr (delayed_force refl_equal), [| type_of_a; a|]))];
           Proofview.Goal.nf_enter { enter = begin fun gl ->
             let concl = Proofview.Goal.concl gl in
-            let concl = EConstr.of_constr concl in
             let env = Proofview.Goal.env gl in
             (** FIXME: this looks really wrong. Does anybody really use this tactic? *)
             let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) concl in
@@ -761,14 +760,14 @@ let  mkCaseEq a  : unit Proofview.tactic =
 
 let case_eq_intros_rewrite x =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
-  let n = nb_prod (Tacmach.New.project gl) (EConstr.of_constr (Proofview.Goal.concl gl)) in
+  let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in
   (* Pp.msgnl (Printer.pr_lconstr x); *)
   Tacticals.New.tclTHENLIST [
       mkCaseEq x;
     Proofview.Goal.nf_enter { enter = begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let hyps = Tacmach.New.pf_ids_of_hyps gl in
-      let n' = nb_prod (Tacmach.New.project gl) (EConstr.of_constr concl) in
+      let n' = nb_prod (Tacmach.New.project gl) concl in
       let h = Tacmach.New.of_old (fun g -> fresh_id hyps (Id.of_string "heq") g) gl in
       Tacticals.New.tclTHENLIST [
                     Tacticals.New.tclDO (n'-n-1) intro;
@@ -809,7 +808,7 @@ let destauto_in id =
   end }
 
 TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (EConstr.of_constr (Proofview.Goal.concl gl)) end } ]
+| [ "destauto" ] -> [ Proofview.Goal.nf_enter { enter = begin fun gl -> destauto (Proofview.Goal.concl gl) end } ]
 | [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
 END
 
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index d4b84284f8..a983a4fea7 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -92,12 +92,10 @@ let rec eq_constr_mod_evars sigma x y =
 let progress_evars t =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let concl = EConstr.of_constr concl in
     let check =
       Proofview.Goal.nf_enter { enter = begin fun gl' ->
         let sigma = Tacmach.New.project gl' in
         let newconcl = Proofview.Goal.concl gl' in
-        let newconcl = EConstr.of_constr newconcl in
         if eq_constr_mod_evars sigma concl newconcl
         then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)")
         else Proofview.tclUNIT ()
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 119e872f8d..4c350b0938 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1595,7 +1595,6 @@ let rec insert_dependent env sigma decl accu hyps = match hyps with
 let assert_replacing id newt tac = 
   let prf = Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let concl = EConstr.of_constr concl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ctx = Environ.named_context env in
@@ -1665,7 +1664,6 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
-    let concl = EConstr.of_constr concl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = match clause with
@@ -2143,10 +2141,9 @@ let get_hyp gl (c,l) clause l2r =
   let env = Tacmach.New.pf_env gl in
   let sigma, hi = decompose_applied_relation env evars (c,l) in
   let but = match clause with
-    | Some id -> Tacmach.New.pf_get_hyp_typ id gl
-    | None -> Evarutil.nf_evar evars (Tacmach.New.pf_concl gl)
+    | Some id -> EConstr.of_constr (Tacmach.New.pf_get_hyp_typ id gl)
+    | None -> nf_evar evars (Tacmach.New.pf_concl gl)
   in
-  let but = EConstr.of_constr but in
   unification_rewrite l2r hi.c1 hi.c2 sigma hi.prf hi.car hi.rel but env
 
 let general_rewrite_flags = { under_lambdas = false; on_morphisms = true }
@@ -2195,7 +2192,6 @@ let setoid_proof ty fn fallback =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
-    let concl = EConstr.of_constr concl in
     Proofview.tclORELSE
       begin
         try
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 3ed40357ee..572fa32b74 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1536,7 +1536,6 @@ and interp_match_goal ist lz lr lmr =
       let hyps = Proofview.Goal.hyps gl in
       let hyps = if lr then List.rev hyps else hyps in
       let concl = Proofview.Goal.concl gl in
-      let concl = EConstr.of_constr concl in
       let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
       interp_match_successes lz ist (Tactic_matching.match_goal env sigma hyps concl ilr)
     end }
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index 5cbddc7f64..be1123d5c9 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -51,6 +51,7 @@ let db_pr_goal gl =
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
   let penv = print_named_context env in
+  let concl = EConstr.Unsafe.to_constr concl in
   let pc = print_constr_env env concl in
     str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++