diff options
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 5f003b74bd..a28f4597cf 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -934,11 +934,12 @@ module Search = struct try (* Instance may try to call this before a proof is set up! Thus, give_me_the_proof will fail. Beware! *) - let name, poly = try - let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in - name, poly - with | Proof_global.NoCurrentProof -> - Id.of_string "instance", false + let name, poly = + (* try + * let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in + * name, poly + * with | Proof_global.NoCurrentProof -> *) + Id.of_string "instance", false in let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply ~name ~poly env tac pv |