From 9d0011125da2b24ccf006154ab205c6987fb03d2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 8 Oct 2014 10:33:20 +0200
Subject: library/opaqueTables: enable their use in interactive mode

Before this patch opaque tables were only growing, making them unusable
in interactive mode (leak on Undo).

With this patch the opaque tables are functional and part of the env.
I.e. a constant_body can point to the proof term in 2 ways:
  1) directly (before the constant is discharged)
  2) indirectly, via an int, that is mapped by the opaque table to
     the proof term.
This is now consistent in batch/interactive mode

This is step 0 to make an interactive coqtop able to dump a .vo/.vi
---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index b613a4b13c..71ebf49233 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -763,7 +763,7 @@ let make_graph (f_ref:global_reference) =
       | _ -> raise (UserError ("", str "Not a function reference") )
   in
   Dumpglob.pause ();
-  (match body_of_constant c_body with
+  (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom !"
      | Some body ->
 	 let env = Global.env () in
-- 
cgit v1.2.3