From aa1022af5ec9970c8251d2bc3b074ae128e9e163 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 9 Mar 2009 19:47:26 +0000
Subject: Optionally list opaque constants in addition to axions/variables in
 assumptions. Feel free to rename "Print Opaque Dependencies" to something
 better.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.mli | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'kernel/environ.mli')

diff --git a/kernel/environ.mli b/kernel/environ.mli
index b0dc2846f9..9e1afdf19b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
+  | Opaque of constant     (* An opaque constant. *)
 
 (* AssumptionSet.t is a set of [assumption] *)
 module OrderedContextObject :  Set.OrderedType with type t = context_object
 module ContextObjectMap : Map.S with type key = context_object
 
-(* collects all the assumptions on which a term relies (together with
-   their type *)
-val assumptions : constr -> env -> Term.types ContextObjectMap.t
+(* collects all the assumptions (optionally including opaque definitions) 
+   on which a term relies (together with their type) *)
+val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t
 
 
-- 
cgit v1.2.3