diff options
| author | Hugo Herbelin | 2014-06-24 02:01:52 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-28 18:52:55 +0200 |
| commit | efa921c807e48cfc19943d2bfd7f4eb11f8f9e09 (patch) | |
| tree | 5984eeff9ad901d9b59bcc76618c5ff184b1b45d /tactics | |
| parent | 820dd1fa1c5d701c5f9af6e456b066d97a0d0499 (diff) | |
Extra check for indirect dependency when abstracting a term which is
not a variable, in the future objective to factorize code between
"generalize dependent" and "set", "destruct", etc.
Diffstat (limited to 'tactics')
| -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 450b48d455..30568edab4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -660,11 +660,6 @@ let rec intros_move = function Tacticals.New.tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false false) (intros_move rest) -let dependent_in_decl a (_,c,t) = - match c with - | None -> dependent a t - | Some body -> dependent a body || dependent a t - (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) |