diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 18:59:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-08 19:59:03 +0200 |
| commit | f461e7657cab9917c5b405427ddba3d56f197efb (patch) | |
| tree | 467ac699f78d0360b05174238aeb1177da892503 /ltac/tacinterp.ml | |
| parent | 9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff) | |
Removing dead code and unused opens.
Diffstat (limited to 'ltac/tacinterp.ml')
| -rw-r--r-- | ltac/tacinterp.ml | 13 |
1 files changed, 1 insertions, 12 deletions
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 31bccd019..6a5d1380d 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -21,7 +21,6 @@ open Libnames open Globnames open Nametab open Pfedit -open Proof_type open Refiner open Tacmach.New open Tactic_debug @@ -35,8 +34,6 @@ open Stdarg open Constrarg open Printer open Pretyping -module Monad_ = Monad -open Evd open Misctypes open Locus open Tacintern @@ -196,7 +193,7 @@ module Value = struct | OptArg t -> Val.Opt (tag_of_arg t) | PairArg (t1, t2) -> Val.Pair (tag_of_arg t1, tag_of_arg t2) - let rec val_cast arg v = prj (tag_of_arg arg) v + let val_cast arg v = prj (tag_of_arg arg) v let cast (Topwit wit) v = val_cast wit v @@ -695,13 +692,6 @@ let pf_interp_casted_constr ist gl c = let pf_interp_constr ist gl = interp_constr ist (pf_env gl) (project gl) -let new_interp_constr ist c k = - let open Proofview in - Proofview.Goal.s_enter { s_enter = begin fun gl -> - let (sigma, c) = interp_constr ist (Goal.env gl) (project gl) c in - Sigma.Unsafe.of_pair (k c, sigma) - end } - let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = try match dest_fun x with @@ -1290,7 +1280,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with Ftactic.run tac (fun () -> Proofview.tclUNIT ()) | TacML (loc,opn,l) -> - let open Ftactic.Notations in let trace = push_trace (loc,LtacMLCall tac) ist in let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in let tac = Tacenv.interp_ml_tactic opn in |