From 58630ad9a0b94a804a39a3d99f982965292692c7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 21 May 2018 23:54:55 +0200 Subject: [api] Misctypes removal: miscellaneous aliases. --- interp/genredexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/genredexpr.ml') diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 80697461a..983493b25 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of Misctypes.lident * 'a + | ConstrContext of Names.lident * 'a | ConstrTypeOf of 'a open Libnames -- cgit v1.2.3