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/tacexpr.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'plugins/ltac/tacexpr.ml') diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index f4dd85bc2..d51de8c65 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -15,7 +15,6 @@ open Libnames open Genredexpr open Genarg open Pattern -open Misctypes open Tactypes open Locus @@ -306,7 +305,7 @@ constraint 'a = < type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr -type g_cst = evaluable_global_reference and_short_name or_var +type g_cst = evaluable_global_reference Stdarg.and_short_name or_var type g_ref = ltac_constant located or_var type g_nam = lident -- cgit v1.2.3