portage Omega (code seulement)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@381 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 96 insertions, 78 deletions

diff --git a/.depend b/.depend
index 48e03e97e5..1cd80335d6 100644
--- a/.depend
+++ b/.depend
@@ -32,6 +32,8 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
     kernel/names.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi 
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
+lib/system.cmi: lib/pp.cmi 
+lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
 library/global.cmi: kernel/constant.cmi kernel/environ.cmi \
@@ -47,8 +49,6 @@ library/library.cmi: lib/pp.cmi
 library/nametab.cmi: kernel/names.cmi 
 library/redinfo.cmi: kernel/names.cmi kernel/term.cmi 
 library/summary.cmi: kernel/names.cmi 
-lib/system.cmi: lib/pp.cmi 
-lib/util.cmi: lib/pp.cmi 
 parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     parsing/pcoq.cmi lib/pp.cmi 
 parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \
@@ -71,10 +71,6 @@ parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
 parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \
     pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi 
-pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
-    kernel/evd.cmi kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi \
-    lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi 
 pretyping/class.cmi: pretyping/classops.cmi library/declare.cmi \
@@ -90,8 +86,6 @@ pretyping/evarconv.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
     kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi 
 pretyping/evarutil.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
     kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi 
-pretyping/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \
-    kernel/names.cmi kernel/term.cmi 
 pretyping/multcase.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
     kernel/evd.cmi kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi 
 pretyping/pretype_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
@@ -149,9 +143,9 @@ tactics/hiddentac.cmi: kernel/names.cmi proofs/proof_trees.cmi \
 tactics/inv.cmi: parsing/coqast.cmi kernel/names.cmi proofs/tacmach.cmi 
 tactics/nbtermdn.cmi: tactics/btermdn.cmi kernel/generic.cmi \
     pretyping/rawterm.cmi kernel/term.cmi 
-tactics/pattern.cmi: kernel/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi tactics/stock.cmi kernel/term.cmi \
-    lib/util.cmi 
+tactics/pattern.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
+    proofs/proof_trees.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    tactics/stock.cmi kernel/term.cmi lib/util.cmi 
 tactics/stock.cmi: kernel/names.cmi 
 tactics/tacentries.cmi: proofs/proof_trees.cmi proofs/tacmach.cmi 
 tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \
@@ -181,11 +175,11 @@ toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
+toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 toplevel/vernacentries.cmi: kernel/names.cmi kernel/term.cmi \
     toplevel/vernacinterp.cmi 
 toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \
     proofs/proof_trees.cmi 
-toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
@@ -302,22 +296,30 @@ lib/dyn.cmo: lib/util.cmi lib/dyn.cmi
 lib/dyn.cmx: lib/util.cmx lib/dyn.cmi 
 lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi 
 lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi 
-lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
-lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gmap.cmo: lib/gmap.cmi 
 lib/gmap.cmx: lib/gmap.cmi 
+lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi 
+lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi 
 lib/gset.cmo: lib/gset.cmi 
 lib/gset.cmx: lib/gset.cmi 
 lib/hashcons.cmo: lib/hashcons.cmi 
 lib/hashcons.cmx: lib/hashcons.cmi 
 lib/options.cmo: lib/util.cmi lib/options.cmi 
 lib/options.cmx: lib/util.cmx lib/options.cmi 
-lib/pp_control.cmo: lib/pp_control.cmi 
-lib/pp_control.cmx: lib/pp_control.cmi 
 lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi 
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
+lib/pp_control.cmo: lib/pp_control.cmi 
+lib/pp_control.cmx: lib/pp_control.cmi 
 lib/profile.cmo: lib/system.cmi lib/profile.cmi 
 lib/profile.cmx: lib/system.cmx lib/profile.cmi 
+lib/stamps.cmo: lib/stamps.cmi 
+lib/stamps.cmx: lib/stamps.cmi 
+lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
+lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
+lib/util.cmo: lib/pp.cmi lib/util.cmi 
+lib/util.cmx: lib/pp.cmx lib/util.cmi 
 library/declare.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi library/impargs.cmi \
     library/indrec.cmi kernel/inductive.cmi library/lib.cmi \
@@ -390,14 +392,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \
     library/summary.cmi 
 library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \
     library/summary.cmi 
-lib/stamps.cmo: lib/stamps.cmi 
-lib/stamps.cmx: lib/stamps.cmi 
-lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
-lib/system.cmx: lib/pp.cmx lib/util.cmx lib/system.cmi 
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi 
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi 
-lib/util.cmo: lib/pp.cmi lib/util.cmi 
-lib/util.cmx: lib/pp.cmx lib/util.cmi 
 parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi lib/hashcons.cmi \
     kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi 
 parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx lib/hashcons.cmx \
@@ -564,28 +558,6 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     pretyping/pretype_errors.cmx kernel/reduction.cmx pretyping/retyping.cmx \
     kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     pretyping/evarutil.cmi 
-pretyping/indrec.cmo: kernel/environ.cmi kernel/generic.cmi \
-    kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \
-    kernel/typeops.cmi lib/util.cmi pretyping/indrec.cmi 
-pretyping/indrec.cmx: kernel/environ.cmx kernel/generic.cmx \
-    kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
-    kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \
-    kernel/typeops.cmx lib/util.cmx pretyping/indrec.cmi 
-pretyping/oldcases.cmo: kernel/environ.cmi pretyping/evarconv.cmi \
-    pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
-    library/global.cmi library/indrec.cmi kernel/inductive.cmi \
-    kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
-    pretyping/pretype_errors.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
-    pretyping/retyping.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi 
-pretyping/oldcases.cmx: kernel/environ.cmx pretyping/evarconv.cmx \
-    pretyping/evarutil.cmx kernel/evd.cmx kernel/generic.cmx \
-    library/global.cmx library/indrec.cmx kernel/inductive.cmx \
-    kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
-    pretyping/pretype_errors.cmx pretyping/rawterm.cmx kernel/reduction.cmx \
-    pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
-    kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx 
 pretyping/pretype_errors.cmo: kernel/environ.cmi library/global.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \
     kernel/type_errors.cmi pretyping/pretype_errors.cmi 
@@ -881,17 +853,17 @@ tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \
 tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \
     library/declare.cmi kernel/environ.cmi kernel/generic.cmi \
     library/global.cmi library/indrec.cmi kernel/inductive.cmi \
-    proofs/logic.cmi kernel/names.cmi tactics/pattern.cmi lib/pp.cmi \
-    parsing/pretty.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
-    kernel/sign.cmi proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \
+    kernel/names.cmi tactics/pattern.cmi lib/pp.cmi parsing/pretty.cmi \
+    proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
+    proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \
     parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \
     tactics/tacticals.cmi 
 tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \
     library/declare.cmx kernel/environ.cmx kernel/generic.cmx \
     library/global.cmx library/indrec.cmx kernel/inductive.cmx \
-    proofs/logic.cmx kernel/names.cmx tactics/pattern.cmx lib/pp.cmx \
-    parsing/pretty.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
-    kernel/sign.cmx proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \
+    kernel/names.cmx tactics/pattern.cmx lib/pp.cmx parsing/pretty.cmx \
+    proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
+    proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \
     parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \
     tactics/tacticals.cmi 
 tactics/tactics.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \
@@ -936,8 +908,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \
     proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     tactics/wcclausenv.cmi 
-tools/coqdep.cmo: config/coq_config.cmi 
-tools/coqdep.cmx: config/coq_config.cmx 
+tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo 
+tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx 
+tools/coqdep_lexer.cmo: config/coq_config.cmi 
+tools/coqdep_lexer.cmx: config/coq_config.cmx 
+tools/gallina.cmo: tools/gallina_lexer.cmo 
+tools/gallina.cmx: tools/gallina_lexer.cmx 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \
     parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi library/indrec.cmi \
@@ -1050,6 +1026,14 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmi \
     toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: toplevel/usage.cmi 
 toplevel/usage.cmx: toplevel/usage.cmi 
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
+    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernac.cmi 
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
+    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
     library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
@@ -1086,11 +1070,21 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx lib/dyn.cmx \
     toplevel/himsg.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     proofs/proof_trees.cmx proofs/tacinterp.cmx lib/util.cmx \
     toplevel/vernacinterp.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
-    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
-    lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx \
-    library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernac.cmi 
+contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \
+    parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \
+    tactics/equality.cmi kernel/generic.cmi library/global.cmi \
+    kernel/inductive.cmi kernel/names.cmi contrib/omega/omega.cmo \
+    tactics/pattern.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi \
+    tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi 
+contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \
+    parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \
+    tactics/equality.cmx kernel/generic.cmx library/global.cmx \
+    kernel/inductive.cmx kernel/names.cmx contrib/omega/omega.cmx \
+    tactics/pattern.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \
+    kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx \
+    tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx 
+contrib/omega/omega.cmo: lib/util.cmi 
+contrib/omega/omega.cmx: lib/util.cmx 
diff --git a/Makefile b/Makefile
index 9ece34b016..9911277a6f 100644
--- a/Makefile
+++ b/Makefile
@@ -28,7 +28,8 @@ noargument:
 ###########################################################################
 
 LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
-              -I proofs -I tactics -I pretyping -I parsing -I toplevel
+              -I proofs -I tactics -I pretyping -I parsing -I toplevel  \
+              -I contrib/omega
 INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
 BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
@@ -41,7 +42,8 @@ OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
 CAMLP4IFDEF=camlp4o pa_ifdef.cmo -D$(OSTYPE)
 
-COQINCLUDES=-I parsing -I theories/Init -I theories/Logic -I theories/Arith \
+COQINCLUDES=-I parsing -I contrib/omega \
+            -I theories/Init -I theories/Logic -I theories/Arith \
             -I theories/Bool -I theories/Zarith
 
 ###########################################################################
@@ -111,11 +113,13 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
 HIGHTACTICS=tactics/dhyp.cmo tactics/auto.cmo # tactics/equality.cmo \
 #            tactics/tauto.cmo 
 
+CONTRIB=contrib/omega/omega.cmo contrib/omega/coq_omega.cmo
+
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
 
 CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \
-    $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS)
+    $(PROOFS) $(TACTICS) $(TOPLEVEL) $(HIGHTACTICS) $(CONTRIB)
 CMX=$(CMO:.cmo=.cmx) $(ARITHSYNTAX:.cmo=.cmx)
 
 ###########################################################################
@@ -251,6 +255,23 @@ clean::
 	rm -f theories/*/*.vo theories/*/*~
 	rm -f tactics/*.vo tactics/*~
 
+
+###########################################################################
+# contribs
+###########################################################################
+
+CONTRIBVO = contrib/omega/Omega.vo       contrib/omega/Zlogarithm.vo \
+            contrib/omega/OmegaSyntax.vo contrib/omega/Zpower.vo \
+            contrib/omega/Zcomplements.vo
+
+contrib: $(CONTRIBVO)
+
+clean::
+	rm -f contrib/*/*~ contrib/*/*.cm[io]
+
+archclean::
+	rm -f contrib/*/*.cmx contrib/*/*.[so]
+
 ###########################################################################
 # tools
 ###########################################################################
@@ -361,13 +382,10 @@ tags:
 # lexer (compiled with camlp4 to get optimized streams)
 
 parsing/lexer.cmo: parsing/lexer.ml
-	$(OCAMLC) $(BYTEFLAGS) -pp "camlp4o pa_ifdef.cmo" -c $<
+	$(OCAMLC_P4O) -c $<
 
 parsing/lexer.cmx: parsing/lexer.ml
-	$(OCAMLOPT) $(OPTFLAGS) -pp "camlp4o pa_ifdef.cmo" -c $<
-
-parsing/lexer.cmi: parsing/lexer.mli
-	$(OCAMLC) $(BYTEFLAGS) -pp "camlp4o pa_ifdef.cmo" -c $<
+	$(OCAMLOPT_P4O) -c $<
 
 clean::
 	rm -f parsing/lexer.ml
@@ -477,7 +495,7 @@ archclean::
 	rm -f toplevel/*.cmx toplevel/*.[so]
 	rm -f tools/*.cmx tools/*.[so]
 	rm -f coqtop.opt coqtop.byte minicoq
-	rm -f scripts/*.cmx scripts/*~
+	rm -f scripts/*.cmx
 
 clean:: archclean
 	rm -f *~
@@ -504,7 +522,7 @@ cleanconfig::
 alldepend: depend dependcoq dependcamlp4
 
 depend: beforedepend
-	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*.ml > .depend
+	$(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend
 
 dependcoq: beforedepend
 	tools/coqdep $(COQINCLUDES) */*.v */*/*.v > .depend.coq
diff --git a/library/declare.ml b/library/declare.ml
index 51748a0204..2ccd77cf09 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -238,8 +238,7 @@ let construct_operator env sp id =
 
 let global_operator sp id = construct_operator (Global.env()) sp id
 
-let construct_reference env kind id =
-  let sp = Nametab.sp_of_id kind id in
+let construct_sp_reference env sp id =
   try
     let (oper,hyps) = construct_operator env sp id in
     let hyps' = Global.var_context () in
@@ -250,7 +249,15 @@ let construct_reference env kind id =
   with Not_found -> 
     VAR (let _ = Environ.lookup_var id env in id)
 
-let global_reference kind id = construct_reference (Global.env()) kind id
+let construct_reference env kind id =
+  let sp = Nametab.sp_of_id kind id in
+  construct_sp_reference env sp id
+
+let global_sp_reference sp id = 
+  construct_sp_reference (Global.env()) sp id
+
+let global_reference kind id = 
+  construct_reference (Global.env()) kind id
 
 let global_reference_imps kind id =
   let c = global_reference kind id in
diff --git a/library/declare.mli b/library/declare.mli
index 470d6dee9d..0142eb0ac6 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -65,6 +65,8 @@ val global_operator : section_path -> identifier -> sorts oper * var_context
     [construct_reference] is a version which looks for variables in a 
     given environment instead of looking in the current global environment. *)
 
+val global_sp_reference : section_path -> identifier -> constr
+
 val global_reference : path_kind -> identifier -> constr
 val global_reference_imps : path_kind -> identifier -> constr * int list
 
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 6c99238f4f..2c7351bf10 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -15,10 +15,7 @@ val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
 
 val add_token : Token.pattern -> unit
 
-ifdef CAMLP4_300 then
 val tparse : string * string -> ((string * string) Stream.t -> string) option
-else
-val tparse : string * string -> (string * string) Stream.t -> string
 
 val token_text : string * string -> string