diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-27 20:42:44 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-27 20:45:06 +0100 |
commit | fc1b3ef9d7270938cd83c524aae0383093b7a4b5 (patch) | |
tree | 9730c1cb313c2b9a510a5030291292353cd41331 | |
parent | 46969b0ece809598b4dd35c688a8ba5237b01efd (diff) |
Removing the unused field ltacrecvars of tactic internalization.
-rw-r--r-- | interp/constrintern.ml | 1 | ||||
-rw-r--r-- | interp/genintern.ml | 1 | ||||
-rw-r--r-- | interp/genintern.mli | 1 | ||||
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 | ||||
-rw-r--r-- | tactics/tacintern.ml | 12 | ||||
-rw-r--r-- | tactics/tacintern.mli | 1 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 6 |
7 files changed, 6 insertions, 18 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 68f0050d4..5151d2a10 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1567,7 +1567,6 @@ let internalize globalenv env allow_patvar lvar c = let lvars = Id.Set.union lvars env.ids in let ist = { Genintern.ltacvars = lvars; - ltacrecvars = Id.Map.empty; genv = globalenv; } in let (_, glb) = Genintern.generic_intern ist gen in diff --git a/interp/genintern.ml b/interp/genintern.ml index c78b13a8f..7795946d5 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -12,7 +12,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; - ltacrecvars : Nametab.ltac_constant Id.Map.t; genv : Environ.env } type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb diff --git a/interp/genintern.mli b/interp/genintern.mli index 6e63f71c5..28f4f530b 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -12,7 +12,6 @@ open Genarg type glob_sign = { ltacvars : Id.Set.t; - ltacrecvars : Nametab.ltac_constant Id.Map.t; genv : Environ.env } (** {5 Internalization functions} *) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 9d25681dc..c61079e63 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1454,7 +1454,7 @@ let do_instr raw_instr pts = let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in let gl = { it=List.hd gls ; sigma=sigma; } in let env= pf_env gl in - let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = env} in + let ist = {ltacvars = Id.Set.empty; genv = env} in let glob_instr = intern_proof_instr ist raw_instr in let instr = interp_proof_instr (get_its_info gl) env sigma glob_instr in diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c8b9a2084..5cc4c835b 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -48,12 +48,10 @@ let error_tactic_expected loc = type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - ltacrecvars : ltac_constant Id.Map.t; - (* ltac recursive names *) genv : Environ.env } let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env } + { ltacvars = Id.Set.empty; genv = Environ.empty_env } let make_empty_glob_sign () = { fully_empty_glob_sign with genv = Global.env () } @@ -64,8 +62,6 @@ let find_ident id ist = Id.Set.mem id ist.ltacvars || Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv)) -let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars - (* a "var" is a ltac var or a var introduced by an intro tactic *) let find_var id ist = Id.Set.mem id ist.ltacvars @@ -116,9 +112,7 @@ let intern_ltac_variable ist = function if find_var id ist then (* A local variable of any type *) ArgVar (loc,id) - else - (* A recursive variable *) - ArgArg (loc,find_recvar id ist) + else raise Not_found | _ -> raise Not_found @@ -801,7 +795,7 @@ let glob_tactic_env l env x = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check (intern_pure_tactic - { ltacvars; ltacrecvars = Id.Map.empty; genv = env }) + { ltacvars; genv = env }) x let split_ltac_fun = function diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 2e662e582..a6e28d568 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -19,7 +19,6 @@ open Nametab type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; - ltacrecvars : ltac_constant Id.Map.t; genv : Environ.env } val fully_empty_glob_sign : glob_sign diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index af541b8b9..8826875a3 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2251,8 +2251,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { - ltacvars; ltacrecvars = Id.Map.empty; - genv = env } t) + ltacvars; genv = env } t) end let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -2262,8 +2261,7 @@ let _ = Proof_global.set_interp_tac interp (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = let hide_interp env = - let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - genv = env } in + let ist = { ltacvars = Id.Set.empty; genv = env } in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with |