From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 15:06:26 +0100
Subject: [location] Use located in misctypes.

---
 plugins/funind/invfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 94ec0a898a..8da4f9233e 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -31,8 +31,8 @@ module RelDecl = Context.Rel.Declaration
 
 let pr_binding prc  =
   function
-    | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
-    | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
 
 let pr_bindings prc prlc = function
   | ImplicitBindings l ->
-- 
cgit v1.2.3


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.
---
 plugins/funind/invfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8da4f9233e..e4536278c0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -274,7 +274,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       List.map
 	(fun decl ->
 	   List.map
-	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
+	     (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
-- 
cgit v1.2.3