diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacmach.ml | 8 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
2 files changed, 0 insertions, 9 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 68cd194799..7fd7aabe40 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -217,14 +217,6 @@ let mutual_fix f n others gl = let mutual_cofix f others gl = with_check (refiner (Prim (Cofix (f,others)))) gl -let rename_bound_var_goal gls = - let { evar_hyps = sign; evar_concl = cl } = sig_it gls in - let ids = ids_of_named_context (named_context_of_val sign) in - convert_concl_no_check - (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls - - - (* Versions with consistency checks *) let introduction id = with_check (introduction_no_check id) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index ed95ef285a..6b6305a177 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -136,7 +136,6 @@ val rename_hyp_no_check : (identifier*identifier) list -> tactic val mutual_fix : identifier -> int -> (identifier * int * constr) list -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> tactic -val rename_bound_var_goal : tactic (*s The most primitive tactics with consistency and type checking *) |