Factorizing code for untyped constr evaluation.

3 files changed, 34 insertions, 26 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index dce7a1860..8a5267541 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -347,22 +347,14 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-let refine_tac simple {Glob_term.closure=closure;term=term} =
+let refine_tac ist simple c =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags = Pretyping.all_no_fail_flags in
-    let tycon = Pretyping.OfType concl in
-    let lvar = { Pretyping.empty_lvar with
-      Pretyping.ltac_constrs = closure.Glob_term.typed;
-      Pretyping.ltac_uconstrs = closure.Glob_term.untyped;
-      Pretyping.ltac_idents = closure.Glob_term.idents;
-    } in
-    let update = { run = begin fun sigma ->
-      let sigma = Sigma.to_evar_map sigma in
-      let (sigma, c) = Pretyping.understand_ltac flags env sigma lvar tycon term in
-      Sigma.Unsafe.of_pair (c, sigma)
-    end } in
+    let expected_type = Pretyping.OfType concl in
+    let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
+    let update = { run = fun sigma -> c.delayed env sigma } in
     let refine = Proofview.Refine.refine ~unsafe:false update in
     if simple then refine
     else refine <*>
@@ -371,11 +363,11 @@ let refine_tac simple {Glob_term.closure=closure;term=term} =
   end }
 
 TACTIC EXTEND refine
-| [ "refine" uconstr(c) ] -> [ refine_tac false c ]
+| [ "refine" uconstr(c) ] -> [ refine_tac ist false c ]
 END
 
 TACTIC EXTEND simple_refine
-| [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ]
+| [ "simple" "refine" uconstr(c) ] -> [ refine_tac ist true c ]
 END
 
 (**********************************************************************)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a0fa9b5f3..0ac115d1d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -685,6 +685,24 @@ let interp_open_constr_list =
 let pf_interp_type ist gl =
   interp_type ist (pf_env gl) (project gl)
 
+(* Fully evaluate an untyped constr *)
+let type_uconstr ?(flags = constr_flags)
+  ?(expected_type = WithoutTypeConstraint) ist c =
+  { delayed = begin fun env sigma ->
+  let open Pretyping in
+  let { closure; term } = c in
+  let vars = {
+    ltac_constrs = closure.typed;
+    ltac_uconstrs = closure.untyped;
+    ltac_idents = closure.idents;
+    ltac_genargs = ist.lfun;
+  } in
+  let sigma = Sigma.to_evar_map sigma in
+  let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
+  Sigma.Unsafe.of_pair (c, sigma)
+  end }
+
+
 (* Interprets a reduction expression *)
 let interp_unfold ist env sigma (occs,qid) =
   (interp_occurrences ist occs,interp_evaluable ist env sigma qid)
@@ -1404,19 +1422,12 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
       end
   | TacPretype c ->
       Ftactic.enter begin fun gl ->
-        let sigma = Tacmach.New.project gl in
+        let sigma = Proofview.Goal.sigma gl in
         let env = Proofview.Goal.env gl in
-        let {closure;term} = interp_uconstr ist env c in
-        let vars = {
-          Pretyping.ltac_constrs = closure.typed;
-          Pretyping.ltac_uconstrs = closure.untyped;
-          Pretyping.ltac_idents = closure.idents;
-          Pretyping.ltac_genargs = ist.lfun;
-        } in
-        let (sigma,c_interp) =
-          Pretyping.understand_ltac constr_flags env sigma vars WithoutTypeConstraint term
-        in
-        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
+        let c = interp_uconstr ist env c in
+        let Sigma (c, sigma, _) = (type_uconstr ist c).delayed env sigma in
+        let sigma = Sigma.to_evar_map sigma in
+        Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c))
       end
   | TacNumgoals ->
       Ftactic.lift begin
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index c67aa31a9..5b81da74a 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -65,6 +65,11 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac
 (** Interprets an expression that evaluates to a constr *)
 val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic
 
+val type_uconstr :
+  ?flags:Pretyping.inference_flags ->
+  ?expected_type:Pretyping.typing_constraint ->
+  interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
+
 (** Interprets redexp arguments *)
 val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr