diff options
| author | herbelin | 2008-02-09 11:31:35 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-09 11:31:35 +0000 |
| commit | bd8b71db33fb9e40575713bc58ae39ccf9f68ab7 (patch) | |
| tree | 4630797ba70528ffeaf076081720866efea3e7dc /proofs | |
| parent | 667de252676eb051fc4e056234f505ebafc335ca (diff) | |
Solde de code mort et petites optimisations sur lesquels je suis
tombé au cours du temps
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10544 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |