diff options
Diffstat (limited to 'plugins/ssr/ssrtacticals.ml')
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 372ae86bd..83581f341 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -14,7 +14,6 @@ open Names open Constr open Termops open Tacmach -open Misctypes open Locusops open Ssrast @@ -25,7 +24,7 @@ module NamedDecl = Context.Named.Declaration (** Tacticals (+, -, *, done, by, do, =>, first, and last). *) -let get_index = function ArgArg i -> i | _ -> +let get_index = function Locus.ArgArg i -> i | _ -> anomaly "Uninterpreted index" (* Toplevel constr must be globalized twice ! *) |