aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-13 11:36:18 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-13 11:36:18 +0000
commita630b49901a26b6c044431942005ae48d6ecf3b7 (patch)
tree89c1cdfdacea246c6c404bbaa0423f21b72db0c8 /parsing
parent3bc2bb21ea017134ebd759062d71c932efb439e1 (diff)
Bug nommage Stdlib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1373 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_natsyntax.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index a4c9d9082..a99046686 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -10,7 +10,7 @@ open Util
open Names
open Coqast
open Ast
-open Coqlib
+open Stdlib
open Termast
exception Non_closed_number