From 48a377680f4f3b96f7c19c22f5641877c561f03d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Jul 2019 13:51:49 +0200
Subject: Declare section variables in direct style "without" an object

The object was mostly for wrangling universes, but we already have the
universe object for that.

It's also used by some code which iterates over objects to find
variables.

Search used to do this but was changed in a previous commit.

Prettyp.print_context and derivatives do this and I don't understand
it enough to fix it, so I kept a dummy object around. It seems like a
not very common used Print family (not documented AFAICT) so maybe we
should remove it all instead.
---
 plugins/funind/indfun_common.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 58b0ead130..ca19116ef0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -128,7 +128,7 @@ let save name const ?hook uctx scope kind =
   let r = match scope with
     | Discharge ->
       let c = SectionLocalDef const in
-      let _ = declare_variable ~name ~kind (Lib.cwd(), c) in
+      let () = declare_variable ~name ~kind (Lib.cwd(), c) in
       VarRef name
     | Global local ->
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
-- 
cgit v1.2.3


From 6e22817c6dab5043f1bdcbb1a1c8da281d4b3d7b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 3 Jul 2019 10:12:04 +0200
Subject: declare_variable: path is always Lib.cwd()

---
 plugins/funind/indfun_common.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ca19116ef0..c906670dc0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -128,7 +128,7 @@ let save name const ?hook uctx scope kind =
   let r = match scope with
     | Discharge ->
       let c = SectionLocalDef const in
-      let () = declare_variable ~name ~kind (Lib.cwd(), c) in
+      let () = declare_variable ~name ~kind c in
       VarRef name
     | Global local ->
       let kn = declare_constant ~name ~kind ~local (DefinitionEntry const) in
-- 
cgit v1.2.3