From bfb42267924cbdafc101ac1cab55ace5e2733bfb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 25 May 2000 14:58:52 +0000
Subject: Petit bug get_current_context

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@475 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f90af433bb..3e5cf4903d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -122,7 +122,7 @@ let print_loadpath () =
 
 let get_goal_context_of_args = function
   | [VARG_NUMBER n] -> get_goal_context n
-  | [] -> get_current_goal_context ()
+  | [] -> get_current_context ()
   | _ -> bad_vernac_args "goal_of_args"
 
 let isfinite = function 
-- 
cgit v1.2.3