diff options
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a29ab24ba..e55ba5d0e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1910,8 +1910,6 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = (intros_move rstatus) (intros_move newlstatus) -let update destopt tophyp = if destopt = MoveLast then tophyp else destopt - let safe_dest_intros_patterns avoid thin dest pat tac gl = try intros_patterns true avoid [] thin dest tac pat gl with UserError ("move_hyp",_) -> @@ -2650,9 +2648,6 @@ let rebuild_elimtype_from_scheme (scheme:elim_scheme): types = paramconcl -exception NoLastArg -exception NoLastArgCcl - (* Builds an elim_scheme from its type and calling form (const+binding). We first separate branches. We obtain branches, hyps before (params + preds), hyps after (args <+ indarg if present>) and conclusion. Then we proceed as |