diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /tactics | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hipattern.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 0 insertions, 3 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 851554b83..15b40b42d 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 let meta3 = mkmeta 3 -let meta4 = mkmeta 4 let op2bool = function Some _ -> true | None -> false diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9c2a1d850..53f8e4d5f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5039,8 +5039,6 @@ end module New = struct open Proofview.Notations - let exact_proof c = exact_proof c - open Genredexpr open Locus |