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.
---
 pretyping/locus.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping/locus.ml')

diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 95a2e495be..37dd120c1a 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -9,10 +9,13 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** Locus : positions in hypotheses and goals *)
 
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
 (** {6 Occurrences} *)
 
 type 'a occurrences_gen =
-- 
cgit v1.2.3