From a7cce63afed99a666cb893430bdc81ed0a6c67c3 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 23 Oct 2006 10:01:40 +0000
Subject: bug #1194: normalisation evars a la sortie de focus

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

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 55a965aee6..c72fb248bd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1025,7 +1025,6 @@ let vernac_backtrack snum pnum naborts =
   (try print_subgoals () with UserError _ -> ())
   
 
-  (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *)
 let vernac_focus gln =
   check_not_proof_mode "No focussing or Unfocussing in Proof Mode.";
   match gln with 
-- 
cgit v1.2.3