diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-29 11:04:52 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-07-29 17:16:29 +0200 |
| commit | dfb5897b99cd21934c5d096c329585367665b986 (patch) | |
| tree | 3ce2cb722844e0c3f4ffef1338cfb4d06ee0276f | |
| parent | 93d3747dd991cbe1e80a026b804794c7da01296e (diff) | |
Clean up obsolete comment.
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9fd1b1c82..b83775b93 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1104,8 +1104,6 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t = interp_external loc ist com req la_interp | TacFreshId l -> GTac.raw_enter begin fun gl -> - (* spiwack: I'm probably being over-conservative here, - pf_interp_fresh_id shouldn't raise exceptions *) let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id)) end |