From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 1 Jun 2018 02:37:15 +0200 Subject: [api] Remove Misctypes. We move the last 3 types to more adequate places. --- plugins/ltac/extraargs.mli | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'plugins/ltac/extraargs.mli') diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index ff697e3c7..737147884 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -12,7 +12,6 @@ open Tacexpr open Names open Constrexpr open Glob_term -open Misctypes val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry @@ -20,9 +19,9 @@ val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type -val occurrences : (int list or_var) Pcoq.Gram.entry -val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type -val pr_occurrences : int list or_var -> Pp.t +val occurrences : (int list Locus.or_var) Pcoq.Gram.entry +val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type +val pr_occurrences : int list Locus.or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences val wit_natural : int Genarg.uniform_genarg_type -- cgit v1.2.3