From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 1 Jun 2018 02:37:15 +0200
Subject: [api] Remove Misctypes.

We move the last 3 types to more adequate places.
---
 proofs/redexpr.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 03ebc3275..629b77be2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -23,7 +23,6 @@ open Tacred
 open CClosure
 open RedFlags
 open Libobject
-open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
@@ -200,8 +199,8 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
-  | ArgArg x -> x
+  | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+  | Locus.ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
-- 
cgit v1.2.3