diff options
| author | Pierre-Marie Pédrot | 2014-11-05 00:56:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-07 18:41:22 +0100 |
| commit | c32728e7bf0ba0449b60ea49df7f92fb6b70923d (patch) | |
| tree | aa4221a0343c0095808010f15fb5dbb1a4efe237 /proofs/tacmach.ml | |
| parent | b320666d84e2f9b91d0ab6dd70f29cdb7da68818 (diff) | |
Removing the legacy intro tactic code.
Diffstat (limited to 'proofs/tacmach.ml')
| -rw-r--r-- | proofs/tacmach.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 5b36052244..03f2fd2b44 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -105,10 +105,6 @@ let pf_matches = pf_apply ConstrMatching.matches_conv let refiner = refiner -(* This does not check that the variable name is not here *) -let introduction_no_check id = - refiner (Intro id) - let internal_cut_no_check replace id t gl = refiner (Cut (true,replace,id,t)) gl @@ -133,7 +129,6 @@ let mutual_cofix f others j gl = (* Versions with consistency checks *) -let introduction id = with_check (introduction_no_check id) let internal_cut b d t = with_check (internal_cut_no_check b d t) let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t) let refine c = with_check (refine_no_check c) |