From 14d27313ae3bdec2a61ce04cee9129b6e6775252 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 11 Mar 2013 21:35:13 +0000
Subject: Obligations generated by Program are now local.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16265 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/obligations.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 74b387dfe9..a088fa1533 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -704,9 +704,9 @@ let dependencies obls n =
       obls;
     !res
 
-let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind = Decl_kinds.Local, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
-let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Local, Decl_kinds.Proof Decl_kinds.Lemma
 
 let kind_of_opacity o =
   match o with
-- 
cgit v1.2.3