From cf04daec997ae431b14dd3a3bbf0db22013b3c71 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Tue, 29 Jul 2014 14:07:42 +0200
Subject: Untyped terms in tactic: function [type_term c] to give a typed
 version of [c].

---
 tactics/tacintern.ml | 3 ++-
 tactics/tacinterp.ml | 9 +++++++++
 tactics/tacsubst.ml  | 1 +
 3 files changed, 12 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 44b695e21..a651d298f 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -631,7 +631,7 @@ and intern_tactic_as_arg loc onlytac ist a =
   | TacCall _ | TacExternal _ | Reference _
   | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a)
   | Tacexp a -> a
-  | ConstrMayEval _ | UConstr _ | TacFreshId _ as a ->
+  | ConstrMayEval _ | UConstr _ | TacFreshId _ | TacPretype _ as a ->
       if onlytac then error_tactic_expected loc else TacArg (loc,a)
   | MetaIdArg _ -> assert false
 
@@ -662,6 +662,7 @@ and intern_tacarg strict onlytac ist = function
   | TacExternal (loc,com,req,la) ->
       TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la)
   | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x)
+  | TacPretype c -> TacPretype (intern_constr ist c)
   | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
   | TacGeneric arg ->
     let (_, arg) = Genintern.generic_intern ist arg in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cb63d53dd..a6f7ff9af 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1135,6 +1135,15 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
         let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in
         GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id))
       end
+  | TacPretype c ->
+      GTac.raw_enter begin fun gl ->
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
+        let c_glob = interp_uconstr ist env c in
+        let (sigma,c_interp) = Pretyping.understand_tcc sigma env c_glob in
+        Proofview.V82.tclEVARS sigma <*>
+        GTac.return (Value.of_constr c_interp)
+      end
   | Tacexp t -> val_interp ist t
   | TacDynamic(_,t) ->
       let tg = (Dyn.tag t) in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0872f8bbf..c0b81e90d 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -261,6 +261,7 @@ and subst_tacarg subst = function
   | TacExternal (_loc,com,req,la) ->
       TacExternal (_loc,com,req,List.map (subst_tacarg subst) la)
   | TacFreshId _ as x -> x
+  | TacPretype c -> TacPretype (subst_glob_constr subst c)
   | Tacexp t -> Tacexp (subst_tactic subst t)
   | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg)
   | TacDynamic(the_loc,t) as x ->
-- 
cgit v1.2.3