diff options
| author | Pierre-Marie Pédrot | 2014-09-04 17:58:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-05 11:59:42 +0200 |
| commit | 466c25ea43149deedf50e0105a6d1e69db91c8fd (patch) | |
| tree | 98d76bc6449162524c713554d9ee76afc55f1de1 /proofs/tacmach.ml | |
| parent | 8c54bdeec740fb9edd80e28ce743418bf1276b90 (diff) | |
Removing the old implementation of clear_body.
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 f87d03183e..6c72009d4c 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -127,10 +127,6 @@ let convert_hyp_no_check d gl = let thin_no_check ids gl = if List.is_empty ids then tclIDTAC gl else refiner (Thin ids) gl -(* This does not check dependencies *) -let thin_body_no_check ids gl = - if List.is_empty ids then tclIDTAC gl else refiner (ThinBody ids) gl - let move_hyp_no_check with_dep id1 id2 gl = refiner (Move (with_dep,id1,id2)) gl @@ -155,7 +151,6 @@ let refine c = with_check (refine_no_check c) let convert_concl d sty = with_check (convert_concl_no_check d sty) let convert_hyp d = with_check (convert_hyp_no_check d) let thin c = with_check (thin_no_check c) -let thin_body c = with_check (thin_body_no_check c) let move_hyp b id id' = with_check (move_hyp_no_check b id id') let rename_hyp l = with_check (rename_hyp_no_check l) |