From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 library/declare.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 31c9c24bc3..6b505ac09c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -512,8 +512,8 @@ let do_constraint poly l =
   let open Misctypes in
   let u_of_id x =
     match x with
-    | GProp -> Loc.dummy_loc, (false, Univ.Level.prop)
-    | GSet -> Loc.dummy_loc, (false, Univ.Level.set)
+    | GProp -> Loc.tag (false, Univ.Level.prop)
+    | GSet  -> Loc.tag (false, Univ.Level.set)
     | GType None ->
        user_err ~hdr:"Constraint"
                      (str "Cannot declare constraints on anonymous universes")
-- 
cgit v1.2.3