diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-05 13:40:18 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-06 10:48:42 +0100 |
commit | fe902cb9235a29427f18c234ffffc9b9070512a1 (patch) | |
tree | 55801193852b70d97521874f3f351d0f867cb05f /tactics/tactics.ml | |
parent | db8fcbb7763ac784f7c72b72509d5dc7c2c5323c (diff) |
[compat] Remove "Shrink Abstract"
Following up on #6791, we the option "Shrink Abstract".
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 17 |
1 files changed, 1 insertions, 16 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b99a45103..b41df7f75 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -89,18 +89,6 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* Shrinking of abstract proofs. *) - -let shrink_abstract = ref true - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "shrinking of abstracted proofs"; - optkey = ["Shrink"; "Abstract"]; - optread = (fun () -> !shrink_abstract) ; - optwrite = (fun b -> shrink_abstract := b) } - (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -4986,10 +4974,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let (_, info) = CErrors.push src in iraise (e, info) in - let const, args = - if !shrink_abstract then shrink_entry sign const - else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) - in + let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in |