Move to OCaml 3.10. Requires debian packages from unstable (soon in testing).

diff --git a/Makefile.defs.in b/Makefile.defs.in
index 804d2489d372c0253492f420d1983ffee4add6c4..faa0c41f448abde5786d9262b5e5d5a46133220d 100644 (file)
--- a/Makefile.defs.in
+++ b/Makefile.defs.in
@@ -3,7 +3,7 @@ OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@
 else
 OCAMLFIND = @OCAMLFIND@
 endif
-CAMLP4O = @CAMLP4O@
+CAMLP5O = @CAMLP5O@
 LABLGLADECC = @LABLGLADECC@
 HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
 DISTRIBUTED = @DISTRIBUTED@

diff --git a/components/METAS/meta.helm-content_pres.src b/components/METAS/meta.helm-content_pres.src
index 1e76f9fe8137c9b781b1a07379479f8b4c667f1c..976b8f10ce76ee48df6d2a1432ff27d79b9a2c88 100644 (file)
--- a/components/METAS/meta.helm-content_pres.src
+++ b/components/METAS/meta.helm-content_pres.src
@@ -1,4 +1,4 @@
-requires="helm-acic_content helm-syntax_extensions camlp4.gramlib ulex helm-grafite"
+requires="helm-acic_content helm-syntax_extensions camlp5.gramlib ulex08 helm-grafite"
 version="0.0.1"
 archive(byte)="content_pres.cma"
 archive(native)="content_pres.cmxa"

diff --git a/components/METAS/meta.helm-extlib.src b/components/METAS/meta.helm-extlib.src
index bfee89e3dbcf1d4ff23ef7436f86b9ffd28256ea..2002fccf1d813bf2161bfa71d9b6201ed83fc265 100644 (file)
--- a/components/METAS/meta.helm-extlib.src
+++ b/components/METAS/meta.helm-extlib.src
@@ -1,4 +1,4 @@
-requires="unix camlp4.gramlib"
+requires="unix camlp5.gramlib"
 version="0.0.1"
 archive(byte)="extlib.cma"
 archive(native)="extlib.cmxa"

diff --git a/components/METAS/meta.helm-grafite_parser.src b/components/METAS/meta.helm-grafite_parser.src
index d921b55889574bd0b971f5262a156e6794a9a217..abf16caeb042ff6fb9a3617766cc59553dafbfd5 100644 (file)
--- a/components/METAS/meta.helm-grafite_parser.src
+++ b/components/METAS/meta.helm-grafite_parser.src
@@ -1,4 +1,4 @@
-requires="helm-lexicon helm-grafite ulex"
+requires="helm-lexicon helm-grafite ulex08"
 version="0.0.1"
 archive(byte)="grafite_parser.cma"
 archive(native)="grafite_parser.cmxa"

diff --git a/components/METAS/meta.helm-lexicon.src b/components/METAS/meta.helm-lexicon.src
index 35ab5dd36b4c5f54a8db3a7ff4f6b5d3a46c822a..741fd603e024df08549b83b54d570a8c40304d74 100644 (file)
--- a/components/METAS/meta.helm-lexicon.src
+++ b/components/METAS/meta.helm-lexicon.src
@@ -1,4 +1,4 @@
-requires="helm-content_pres helm-cic_disambiguation camlp4.gramlib"
+requires="helm-content_pres helm-cic_disambiguation camlp5.gramlib"
 version="0.0.1"
 archive(byte)="lexicon.cma"
 archive(native)="lexicon.cmxa"

diff --git a/components/METAS/meta.helm-syntax_extensions.src b/components/METAS/meta.helm-syntax_extensions.src
index eb25adac0f0b5971044415884ee893e4a75c60a8..f9e210f6e170e1d797b1a9d8c156335eb94b9476 100644 (file)
--- a/components/METAS/meta.helm-syntax_extensions.src
+++ b/components/METAS/meta.helm-syntax_extensions.src
@@ -2,6 +2,6 @@ requires="str"
 version="0.0.1"
 archive(byte)="utf8_macros.cma"
 archive(native)="utf8_macros.cmxa"
-requires(syntax,preprocessor)="camlp4"
+requires(syntax,preprocessor)="camlp5"
 archive(syntax,preprocessor)="pa_extend.cmo pa_unicode_macro.cma profiling_macros.cma"
 linkopts=""

diff --git a/components/Makefile.common b/components/Makefile.common
index 59b35aa7371348377d34bd9d6b4735169b708165..5090dcc78309151231efaa2eee9f923fec0c2c3e 100644 (file)
--- a/components/Makefile.common
+++ b/components/Makefile.common
@@ -11,10 +11,10 @@ H=@
 
 # $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH=
 
-PREPROCOPTIONS = -pp camlp4o
-SYNTAXOPTIONS = -syntax camlp4o
+PREPROCOPTIONS = -pp camlp5o
+SYNTAXOPTIONS = -syntax camlp5o
 PREREQ =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes
 OCAMLDEBUGOPTIONS = -g
 #OCAML_PROF=p -p a
 OCAMLARCHIVEOPTIONS =
@@ -22,7 +22,7 @@ REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE))
 OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
 #OCAMLOPT_DEBUG_FLAGS = -p
 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS) $(OCAMLOPT_DEBUG_FLAGS)
-OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4 $(CAMLP4REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) 
+OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp5 $(CAMLP5REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) 
 OCAMLLEX = ocamllex
 OCAMLYACC = ocamlyacc
 

diff --git a/components/acic_content/cicNotationPt.ml b/components/acic_content/cicNotationPt.ml
index 73eeb017dad00d781bbb61f9242b2eeb8f631186..27ec5734f1a9065aa9762feac57aa20cd31b8771 100644 (file)
--- a/components/acic_content/cicNotationPt.ml
+++ b/components/acic_content/cicNotationPt.ml
@@ -32,7 +32,7 @@ type induction_kind = [ `Inductive | `CoInductive ]
 type sort_kind = [ `Prop | `Set | `Type of CicUniv.universe | `CProp ]
 type fold_kind = [ `Left | `Right ]
 
-type location = Token.flocation
+type location = Stdpp.location
 let fail floc msg =
   let (x, y) = HExtlib.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)

diff --git a/components/binaries/extractor/Makefile b/components/binaries/extractor/Makefile
index 323f405d483699d39f3174063784017f4b00644a..512b13e738d3b6be9e2bad1af9ea9cfb77a62bd6 100644 (file)
--- a/components/binaries/extractor/Makefile
+++ b/components/binaries/extractor/Makefile
@@ -11,22 +11,22 @@ clean:
 extractor: extractor.ml
        $(H)echo "    OCAMLC $<"
        $(H)$(OCAMLFIND) ocamlc \
-               -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+               -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
 
 extractor.opt: extractor.ml
        $(H)echo "    OCAMLOPT $<"
        $(H)$(OCAMLFIND) ocamlopt \
-               -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+               -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
 
 extractor_manager: extractor_manager.ml
        $(H)echo "    OCAMLC $<"
        $(H)$(OCAMLFIND) ocamlc \
-               -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+               -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
 
 extractor_manager.opt: extractor_manager.ml
        $(H)echo "    OCAMLOPT $<"
        $(H)$(OCAMLFIND) ocamlopt \
-               -thread -package mysql,helm-metadata,helm-library -linkpkg -o $@ $<
+               -thread -package mysql,helm-metadata,helm-library -linkpkg -rectypes -o $@ $<
 
 export: extractor.opt extractor_manager.opt
         nice -n 20 \

diff --git a/components/binaries/heights/Makefile b/components/binaries/heights/Makefile
index d989d9c58e774a9d928663293d13e4f6f8ed0f3e..cd270082a6ea82fa86e864e505e1f35d8e651cca 100644 (file)
--- a/components/binaries/heights/Makefile
+++ b/components/binaries/heights/Makefile
@@ -16,8 +16,8 @@ CMXS = $(MLS:%.ml=%.cmx)
 CMIS = $(MLIS:%.mli=%.cmi)
 EXTRAS =
 
-OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg
-OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg
+OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes
+OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes
 OCAMLDEP = $(OCAMLFIND) ocamldep
 OCAMLYACC = ocamlyacc
 OCAMLLEX = ocamllex

diff --git a/components/binaries/table_creator/Makefile b/components/binaries/table_creator/Makefile
index 23e732629abb8b329c1a3771b56cde6ec23f4309..d5889699f46545bc452ef9f3c9d65a8d3b3414f0 100644 (file)
--- a/components/binaries/table_creator/Makefile
+++ b/components/binaries/table_creator/Makefile
@@ -16,7 +16,7 @@ opt: table_creator.opt table_destructor.opt
 table_creator: table_creator.ml 
        $(H)echo "    OCAMLC $<"
        $(H)$(OCAMLFIND) ocamlc \
-               -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+               -thread -package mysql,helm-metadata -linkpkg -rectypes -o $@ $<
 
 table_destructor: table_creator
        $(H)ln -f $< $@
@@ -24,7 +24,7 @@ table_destructor: table_creator
 table_creator.opt: table_creator.ml
        $(H)echo "    OCAMLOPT $<"
        $(H)$(OCAMLFIND) ocamlopt \
-               -thread -package mysql,helm-metadata -linkpkg -o $@ $<
+               -thread -package mysql,helm-metadata -linkpkg -rectypes -o $@ $<
 
 table_destructor.opt: table_creator.opt
        $(H)ln  -f $< $@

diff --git a/components/binaries/transcript/Makefile b/components/binaries/transcript/Makefile
index 7d6cd364ff4cc98628cf5379abd117f008fdafb4..b9bfc6109e2ba69afa2472938ed4b31accf8ce36 100644 (file)
--- a/components/binaries/transcript/Makefile
+++ b/components/binaries/transcript/Makefile
@@ -18,8 +18,8 @@ CMXS = $(MLS:%.ml=%.cmx)
 CMIS = $(MLIS:%.mli=%.cmi)
 EXTRAS =
 
-OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg
-OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg
+OCAMLC = $(OCAMLFIND) ocamlc -thread -package "$(REQUIRES)" -linkpkg -rectypes
+OCAMLOPT = $(OCAMLFIND) ocamlopt -thread -package "$(REQUIRES)" -linkpkg -rectypes
 OCAMLDEP = $(OCAMLFIND) ocamldep
 OCAMLYACC = ocamlyacc
 OCAMLLEX = ocamllex

diff --git a/components/binaries/utilities/Makefile b/components/binaries/utilities/Makefile
index 1874a238543eb464f05813e53a522c2366ec644f..db76fb51da13d904bb3c88bb5348d491cec790e8 100644 (file)
--- a/components/binaries/utilities/Makefile
+++ b/components/binaries/utilities/Makefile
@@ -2,7 +2,7 @@ H=@
 
 UTILITIES = create_environment parse_library list_uris test_library
 UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES))
-LINKOPTS = -linkpkg -thread
+LINKOPTS = -linkpkg -rectypes -thread
 LIBS = helm-cic_proof_checking
 OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS)
 OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS)

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index e93c54808298f14879396fbf637c3444c5bd775f..0b8674c0cf9804b56119107181b6779967468136 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -35,9 +35,9 @@ module Ast = CicNotationPt
 (* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t * bool) list
+  Stdpp.location option * string Lazy.t * bool) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -47,7 +47,7 @@ type aliases = bool * DisambiguateTypes.environment
 type 'a disambiguator_input = string * int * 'a
 
 type domain = domain_tree list
-and domain_tree = Node of Token.flocation list * domain_item * domain
+and domain_tree = Node of Stdpp.location list * domain_item * domain
 
 let rec string_of_domain =
  function
@@ -105,8 +105,8 @@ let descr_of_domain_item = function
 
 type 'a test_result =
   | Ok of 'a * Cic.metasenv
-  | Ko of Token.flocation option * string Lazy.t
-  | Uncertain of Token.flocation option * string Lazy.t
+  | Ko of Stdpp.location option * string Lazy.t
+  | Uncertain of Stdpp.location option * string Lazy.t
 
 let refine_term metasenv context uri term ugraph ~localization_tbl =
 (*   if benchmark then incr actual_refinements; *)

diff --git a/components/cic_disambiguation/disambiguate.mli b/components/cic_disambiguation/disambiguate.mli
index 4fe40da91fb5db8fbe2665df40e73ddca4b17524..5dc0df28b164feaa1d89c880e7cdb3f5323ef0d7 100644 (file)
--- a/components/cic_disambiguation/disambiguate.mli
+++ b/components/cic_disambiguation/disambiguate.mli
@@ -35,9 +35,9 @@
   *   useless for the final user ... *)
 exception NoWellTypedInterpretation of
  int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t * bool) list
+  Stdpp.location option * string Lazy.t * bool) list
 exception PathNotWellFormed
 
 val interpretate_path :

diff --git a/components/cic_disambiguation/disambiguateTypes.ml b/components/cic_disambiguation/disambiguateTypes.ml
index 8263fd3152b8c2c05bb13e7ce25c64e36f53d8c1..150482fbf503df28236aae0c1753d949dd99f135 100644 (file)
--- a/components/cic_disambiguation/disambiguateTypes.ml
+++ b/components/cic_disambiguation/disambiguateTypes.ml
@@ -116,7 +116,7 @@ module type Callbacks =
       UriManager.uri list
     val interactive_interpretation_choice:
       string -> int ->
-      (Token.flocation list * string * string) list list -> int list
+      (Stdpp.location list * string * string) list list -> int list
     val input_or_locate_uri:
       title:string -> ?id:string -> unit -> UriManager.uri option
   end

diff --git a/components/cic_disambiguation/disambiguateTypes.mli b/components/cic_disambiguation/disambiguateTypes.mli
index b584f0bec25437ea993cd3aa35108c171e539e84..96105670108e7d24a184c6042838bfd8659611c6 100644 (file)
--- a/components/cic_disambiguation/disambiguateTypes.mli
+++ b/components/cic_disambiguation/disambiguateTypes.mli
@@ -72,7 +72,7 @@ module type Callbacks =
 
       val interactive_interpretation_choice :
         string -> int ->
-      (Token.flocation list * string * string) list list -> int list
+      (Stdpp.location list * string * string) list list -> int list
 
     (** @param title gtk window title for user prompting
      * @param id unbound identifier which originated this callback invocation *)

diff --git a/components/cic_proof_checking/Makefile b/components/cic_proof_checking/Makefile
index 83b211447141af390419226d2d9dbab858b0d828..b2ee8993f31ebbf6c3d73e3579c711b52894cc56 100644 (file)
--- a/components/cic_proof_checking/Makefile
+++ b/components/cic_proof_checking/Makefile
@@ -25,7 +25,3 @@ EXTRA_OBJECTS_TO_CLEAN =
 
 include ../../Makefile.defs
 include ../Makefile.common
-
-cicReduction.cmo: OCAMLOPTIONS+=-rectypes
-cicReduction.cmx: OCAMLOPTIONS+=-rectypes
-

diff --git a/components/cic_unification/cicRefine.mli b/components/cic_unification/cicRefine.mli
index 30b264455246890438191bc2a1a0a9757db652fa..924020cbb39f771bc4bdea179240fd6b7e858432 100644 (file)
--- a/components/cic_unification/cicRefine.mli
+++ b/components/cic_unification/cicRefine.mli
@@ -31,7 +31,7 @@ exception AssertFailure of string Lazy.t;;
 (* refines [term] and returns the refined form of [term],  *)
 (* its type, the new metasenv and universe graph.          *)
 val type_of_aux':
- ?localization_tbl:Token.flocation Cic.CicHash.t ->
+ ?localization_tbl:Stdpp.location Cic.CicHash.t ->
   Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
    Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
 
@@ -40,7 +40,7 @@ val type_of_aux':
 (* the new metasenv and universe graph.                 *)
 (* the [uri] is required only for inductive definitions *)
 val typecheck : 
- localization_tbl:Token.flocation Cic.CicHash.t ->
+ localization_tbl:Stdpp.location Cic.CicHash.t ->
   Cic.metasenv -> UriManager.uri option -> Cic.obj ->
    Cic.obj * Cic.metasenv * CicUniv.universe_graph
 

diff --git a/components/content_pres/Makefile b/components/content_pres/Makefile
index fb6d0fe46bd9122cb0858b68cb6e2bf487572c5d..2eadef1870dab75156eccace885bd97ae1768d46 100644 (file)
--- a/components/content_pres/Makefile
+++ b/components/content_pres/Makefile
@@ -47,8 +47,8 @@ include ../Makefile.common
 # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by
 # "_loc" occurrences
 UTF8DIR := $(shell $(OCAMLFIND) query helm-syntax_extensions)
-ULEXDIR := $(shell $(OCAMLFIND) query ulex)
-MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
+ULEXDIR := $(shell $(OCAMLFIND) query ulex08)
+MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
 cicNotationLexer.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
 cicNotationParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
 cicNotationLexer.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)

diff --git a/components/content_pres/cicNotationLexer.ml b/components/content_pres/cicNotationLexer.ml
index f157af40696876a7f38b65946cb6c72acc588590..bd071c5b9a6da869dc1384ac7264a5c83ce20bcb 100644 (file)
--- a/components/content_pres/cicNotationLexer.ml
+++ b/components/content_pres/cicNotationLexer.ml
@@ -144,14 +144,8 @@ let error_at_end lexbuf msg =
   raise (Error (begin_cnum, end_cnum, msg))
 
 let return_with_loc token begin_cnum end_cnum =
-  (* TODO handle line/column numbers *)
-  let flocation_begin =
-    { Lexing.pos_fname = "";
-      Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
-      Lexing.pos_cnum = begin_cnum }
-  in
-  let flocation_end = { flocation_begin with Lexing.pos_cnum = end_cnum } in
-  (token, (flocation_begin, flocation_end))
+  let flocation = HExtlib.floc_of_loc (begin_cnum,end_cnum) in
+   token, flocation
 
 let return lexbuf token =
   let begin_cnum, end_cnum = Ulexing.loc lexbuf in
@@ -169,17 +163,17 @@ let mk_lexer token =
 (*     let lexbuf = Ulexing.from_utf8_stream stream in *)
 (** XXX Obj.magic rationale.
  * The problem.
- *  camlp4 constraints the tok_func field of Token.glexer to have type:
+ *  camlp5 constraints the tok_func field of Token.glexer to have type:
  *    Stream.t char -> (Stream.t 'te * flocation_function)
  *  In order to use ulex we have (in theory) to instantiate a new lexbuf each
  *  time a char Stream.t is passed, destroying the previous lexbuf which may
  *  have consumed a character from the old stream which is lost forever :-(
  * The "solution".
- *  Instead of passing to camlp4 a char Stream.t we pass a lexbuf, casting it to
+ *  Instead of passing to camlp5 a char Stream.t we pass a lexbuf, casting it to
  *  char Stream.t with Obj.magic where needed.
  *)
     let lexbuf = Obj.magic stream in
-    Token.make_stream_and_flocation
+    Token.make_stream_and_location
       (fun () ->
         try
           token lexbuf

diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml
index d110bda9a65d10b6cabfc0074a798e5bd7040786..05075f0c3f2f9d8981747e913212fd3dcbcdd8e4 100644 (file)
--- a/components/content_pres/cicNotationParser.ml
+++ b/components/content_pres/cicNotationParser.ml
@@ -224,7 +224,7 @@ let level_of precedence associativity =
   in
   string_of_int precedence ^ assoc_string
 
-type rule_id = Token.t Gramext.g_symbol list
+type rule_id = Grammar.token Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23

diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml
index 9e2277b43041b9f551a67d7ad422369475818d2b..24f0dd1967ab3f8711a5538f61058bcc13417fce 100644 (file)
--- a/components/extlib/hExtlib.ml
+++ b/components/extlib/hExtlib.ml
@@ -403,30 +403,20 @@ let finally at_end f arg =
 
 (** {2 Localized exceptions } *)
 
-exception Localized of Token.flocation * exn
+exception Localized of Stdpp.location * exn
 
-let loc_of_floc = function
-  | { Lexing.pos_cnum = loc_begin }, { Lexing.pos_cnum = loc_end } ->
-      (loc_begin, loc_end)
+let loc_of_floc floc = Stdpp.first_pos floc, Stdpp.last_pos floc;;
 
 let floc_of_loc (loc_begin, loc_end) =
-  let floc_begin =
-    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
-      Lexing.pos_cnum = loc_begin }
-  in
-  let floc_end = { floc_begin with Lexing.pos_cnum = loc_end } in
-  (floc_begin, floc_end)
+ Stdpp.make_loc (loc_begin, loc_end)
 
 let dummy_floc = floc_of_loc (-1, -1)
 
 let raise_localized_exception ~offset floc exn =
- let (x, y) = loc_of_floc floc in
+ let x, y = loc_of_floc floc in
  let x = offset + x in
  let y = offset + y in
- let flocb,floce = floc in
- let floc =
-   { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y }
- in
+ let floc = floc_of_loc (x,y) in
   raise (Localized (floc, exn))
 
 let estimate_size x = 

diff --git a/components/extlib/hExtlib.mli b/components/extlib/hExtlib.mli
index 5f6626b145799af416475cbc407776bab99c62c0..f951a6709817c862d1164a44b060efa8ae52b66a 100644 (file)
--- a/components/extlib/hExtlib.mli
+++ b/components/extlib/hExtlib.mli
@@ -102,14 +102,14 @@ val set_profiling_printings : (string -> bool) -> unit
 
 (** {2 Localized exceptions } *)
 
-exception Localized of Token.flocation * exn
+exception Localized of Stdpp.location * exn
 
-val loc_of_floc: Token.flocation -> int * int
-val floc_of_loc: int * int -> Token.flocation
+val loc_of_floc: Stdpp.location -> int * int
+val floc_of_loc: int * int -> Stdpp.location
 
-val dummy_floc: Lexing.position * Lexing.position
+val dummy_floc: Stdpp.location
 
-val raise_localized_exception: offset:int -> Token.flocation -> exn -> 'a
+val raise_localized_exception: offset:int -> Stdpp.location -> exn -> 'a
 
 (* size in KB (SLOW) *)
 val estimate_size: 'a -> int

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index b0c25bc1e361f2a8ea892bd3686c9b8fa80cbd96..a0bb2e4f95501a7018cf16520fcabafd32e79433 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -27,7 +27,7 @@
 
 type direction = [ `LeftToRight | `RightToLeft ]
 
-type loc = Token.flocation
+type loc = Stdpp.location
 
 type ('term, 'lazy_term, 'ident) pattern =
   'lazy_term option * ('ident * 'term) list * 'term option

diff --git a/components/grafite_parser/Makefile b/components/grafite_parser/Makefile
index 06824b141107f7675b1e33026f011c1096134a3b..eb2f1b1eba2adc4196591163299a2ed86203a71e 100644 (file)
--- a/components/grafite_parser/Makefile
+++ b/components/grafite_parser/Makefile
@@ -18,8 +18,8 @@ clean: clean_tests
 # soon as we have ocaml 3.09 everywhere and "loc" occurrences are replaced by
 # "_loc" occurrences
 UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions)
-ULEXDIR = $(shell $(OCAMLFIND) query ulex)
-MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
+ULEXDIR = $(shell $(OCAMLFIND) query ulex08)
+MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(ULEXDIR) pa_extend.cmo pa_ulex.cma pa_unicode_macro.cma -loc loc"
 grafiteParser.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
 grafiteParser.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
 depend: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)

diff --git a/components/grafite_parser/grafiteDisambiguator.ml b/components/grafite_parser/grafiteDisambiguator.ml
index 4f812ff2f032abae8448782165da6bdc544d5bea..fc2cbc74ef16dd1b3abf82a59609cc3e3f50d136 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguator.ml
+++ b/components/grafite_parser/grafiteDisambiguator.ml
@@ -31,9 +31,9 @@ exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t * bool) list list
+  Stdpp.location option * string Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
 
@@ -42,7 +42,7 @@ type choose_uris_callback =
 
 type choose_interp_callback = 
   string -> int -> 
-    (Token.flocation list * string * string) list list -> int list
+    (Stdpp.location list * string * string) list list -> int list
 
 let mono_uris_callback ~id =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true

diff --git a/components/grafite_parser/grafiteDisambiguator.mli b/components/grafite_parser/grafiteDisambiguator.mli
index f37991f934c8f3b27a9afe247b6afb7feaab8359..88940c2c3818bd40cd30c5e707295ceae1e79bfb 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguator.mli
+++ b/components/grafite_parser/grafiteDisambiguator.mli
@@ -29,9 +29,9 @@ exception Ambiguous_input
 (* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
- ((Token.flocation list * string * string) list *
+ ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Token.flocation option * string Lazy.t * bool) list list
+  Stdpp.location option * string Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 
 (** initially false; for debugging only (???) *)
@@ -39,7 +39,7 @@ val only_one_pass: bool ref
 
 type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = 
-  string -> int -> (Token.flocation list * string * string) list list -> 
+  string -> int -> (Stdpp.location list * string * string) list list -> 
     int list
 
 val set_choose_uris_callback:   choose_uris_callback -> unit

diff --git a/components/lexicon/lexiconAst.ml b/components/lexicon/lexiconAst.ml
index 65bb7ce64657b7a805af49feb64259175972f8b1..5a09d590a86c9c66e5affa57559b88eea5a94b63 100644 (file)
--- a/components/lexicon/lexiconAst.ml
+++ b/components/lexicon/lexiconAst.ml
@@ -27,7 +27,7 @@
 
 type direction = [ `LeftToRight | `RightToLeft ]
 
-type loc = Token.flocation
+type loc = Stdpp.location
 
 type alias_spec =
   | Ident_alias of string * string        (* identifier, uri *)

diff --git a/components/library/refinementTool.ml b/components/library/refinementTool.ml
index e9dae40d945cd62413c08a257530c568d621944f..b78246987b8f6c54ecb32608906267b11264558e 100644 (file)
--- a/components/library/refinementTool.ml
+++ b/components/library/refinementTool.ml
@@ -30,7 +30,7 @@ type type_of_rc =
   (* these are the same functions of cic_unification/ (eventually wrapped) *)
 type kit = {
   type_of_aux':
-    ?localization_tbl:Token.flocation Cic.CicHash.t ->
+    ?localization_tbl:Stdpp.location Cic.CicHash.t ->
     Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
       type_of_rc;
   pack_coercion_obj: Cic.obj -> Cic.obj;

diff --git a/components/syntax_extensions/Makefile b/components/syntax_extensions/Makefile
index 92ed077769c854a97e887852c32f612694e61038..f274c6a8e9605eaf38294a078705a9922bb0d0cf 100644 (file)
--- a/components/syntax_extensions/Makefile
+++ b/components/syntax_extensions/Makefile
@@ -18,18 +18,18 @@ utf8MacroTable.ml:
        ./make_table $@
 utf8MacroTable.cmo: utf8MacroTable.ml
        @echo "  OCAMLC $<"
-       $(H)@$(OCAMLFIND) ocamlc -c $<
+       $(H)@$(OCAMLFIND) ocamlc -c -rectypes $<
 
 pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo
        @echo "  OCAMLC $<"
-       $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o q_MLast.cmo pa_extend.cmo -loc loc" -c $<
+       $(H)@$(OCAMLFIND) ocamlc -package camlp5 -rectypes -pp "camlp5o q_MLast.cmo pa_extend.cmo -loc loc" -c $<
 pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo
        @echo "  OCAMLC -a $@"
        $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^
 
 profiling_macros.cmo: profiling_macros.ml
        @echo "  OCAMLC $<"
-       $(H)@$(OCAMLFIND) ocamlc -package camlp4 -pp "camlp4o -loc loc" -c $<
+       $(H)@$(OCAMLFIND) ocamlc -package camlp5 -pp "camlp5o -loc loc" -c $<
 profiling_macros.cma:profiling_macros.cmo
        @echo "  OCAMLC -a $@"
        $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^
@@ -37,7 +37,7 @@ profiling_macros.cma:profiling_macros.cmo
 
 .PHONY: test
 test: test.ml
-       $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp4o $< -o $@
+       $(OCAMLFIND) ocamlc -package helm-utf8_macros -syntax camlp5o $< -o $@
 
 clean:
 distclean: extra_clean

diff --git a/components/syntax_extensions/README.syntax b/components/syntax_extensions/README.syntax
index 210ecc0954bd0033d3e2f7d2ffa05c89a85e8d1f..eddc7f45b93618f21dd913064c77a08358ca1768 100644 (file)
--- a/components/syntax_extensions/README.syntax
+++ b/components/syntax_extensions/README.syntax
@@ -11,5 +11,5 @@ Sample file:
 
 Compile it with:
 
-  ocamlfind ocamlc -package helm-utf8_macros -syntax camlp4o test.ml
+  ocamlfind ocamlc -package helm-utf8_macros -syntax camlp5o test.ml
 

diff --git a/components/syntax_extensions/pa_unicode_macro.ml b/components/syntax_extensions/pa_unicode_macro.ml
index dda7d4cabc852161144df5a893c1dfc253985d0e..436766862b714ba78af312270b60b669ef0c35f3 100644 (file)
--- a/components/syntax_extensions/pa_unicode_macro.ml
+++ b/components/syntax_extensions/pa_unicode_macro.ml
@@ -28,12 +28,7 @@
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s)
 
-let loc =
-  let dummy_pos =
-    { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
-      Lexing.pos_cnum = -1 }
-  in
-  (dummy_pos, dummy_pos)
+let loc = Stdpp.make_loc (-1, -1)
 
 let expand_unicode_macro macro =
   debug_print (lazy (Printf.sprintf "Expanding macro '%s' ..." macro));

diff --git a/components/tactics/Makefile b/components/tactics/Makefile
index b576f830b5f94909acd7e9f893b8eeff74a2d1fd..c4e020005e0a8ea4462aa678a88e08aa57062bab 100644 (file)
--- a/components/tactics/Makefile
+++ b/components/tactics/Makefile
@@ -42,7 +42,7 @@ tactics.mli: tactics.ml
 
 UTF8DIR = $(shell $(OCAMLFIND) query helm-syntax_extensions)
 STR=$(shell $(OCAMLFIND) query str)
-MY_SYNTAXOPTIONS = -pp "camlp4o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc"
+MY_SYNTAXOPTIONS = -pp "camlp5o -I $(UTF8DIR) -I $(STR) str.cma pa_extend.cmo profiling_macros.cma -loc loc"
 paramodulation/%.cmo: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)
 paramodulation/%.cmo: OCAMLC = $(OCAMLC_P4)
 paramodulation/%.cmx: SYNTAXOPTIONS = $(MY_SYNTAXOPTIONS)

diff --git a/configure.ac b/configure.ac
index 0af17fcad249bb335c600ccb41122254dcb24c27..4e78143996a600968f9154642c3c809b1b369143 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -30,11 +30,11 @@ if test $HAVE_LABLGLADECC = "yes"; then
 else
   AC_MSG_ERROR(could not find lablgladecc2)
 fi
-AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no)
-if test $HAVE_CAMLP4O = "yes"; then
-  CAMLP4O="camlp4o"
+AC_CHECK_PROG(HAVE_CAMLP5O, camlp5o, yes, no)
+if test $HAVE_CAMLP5O = "yes"; then
+  CAMLP5O="camlp5o"
 else
-  AC_MSG_ERROR(could not find camlp4o)
+  AC_MSG_ERROR(could not find camlp5o)
 fi
 
 # look for METAS dir
@@ -168,7 +168,7 @@ if test "yes" = "$DBHOST"; then
 fi
 AC_MSG_RESULT($MSG)
 
-AC_SUBST(CAMLP4O)
+AC_SUBST(CAMLP5O)
 AC_SUBST(DBHOST)
 AC_SUBST(DEBUG)
 AC_SUBST(DISTRIBUTED)

diff --git a/matita/Makefile b/matita/Makefile
index 93a6fc6cbb8a9d7d32a0f769558e76199e942151..923a0f614acfe169e8e36c385ac3c7f2f657c0ab 100644 (file)
--- a/matita/Makefile
+++ b/matita/Makefile
@@ -5,7 +5,7 @@ include ../Makefile.defs
 NULL =
 H=@
 
-OCAML_FLAGS = -pp $(CAMLP4O)
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes
 PKGS = -package "$(MATITA_REQUIRES)"
 CPKGS = -package "$(MATITA_CREQUIRES)"
 OCAML_THREADS_FLAGS = -thread

diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 79521e20650c95f8a2016df8c0e82ae921a432ad..7f76ae0c852f62c5b88d50818c6821894bb84508 100644 (file)
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -175,11 +175,7 @@ intro;
 apply (not_le_Sn_n ? H3).
 qed.
 
-theorem lt_S_S: ∀n,m. n < m → S n < S m.
-intros;
-unfold lt in H;
-apply (le_S_S ? ? H).
-qed.
+
 
 (* moved to nat/order.ma 
 theorem lt_O_S: ∀n. O < S n.

diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 8053d50de55bfe8afc7d434243b17ceca34b9536..42454393ca45cc08676ef8205d878a437a1266f2 100644 (file)
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -100,6 +100,12 @@ theorem lt_S_S_to_lt: \forall n,m.
 intros. apply le_S_S_to_le. assumption.
 qed.
 
+theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
+intros;
+unfold lt in H;
+apply (le_S_S ? ? H).
+qed.
+
 theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
 intros.elim H.exact I.exact I.
 qed.

diff --git a/matita/matitaExcPp.ml b/matita/matitaExcPp.ml
index 339971feaed0d33f73339bb3ce6e25244369cf48..42777735c2b96d4f9d4a6c2d26fb6783cf64417f 100644 (file)
--- a/matita/matitaExcPp.ml
+++ b/matita/matitaExcPp.ml
@@ -96,10 +96,7 @@ let rec to_string =
           let (x, y) = HExtlib.loc_of_floc floc in
           let x = x + offset in
           let y = y + offset in
-          let flocb,floce = floc in
-          let floc =
-           {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y}
-          in
+          let floc = HExtlib.floc_of_loc (x,y) in
            Some floc
        | _ -> None in
      let rec explain =

diff --git a/matita/matitaExcPp.mli b/matita/matitaExcPp.mli
index 9d8c7739fc59f2514bd51ea5e6088d0a98f0e1f8..4abe0b4f9d5bc6956171e5459a289b0203c14502 100644 (file)
--- a/matita/matitaExcPp.mli
+++ b/matita/matitaExcPp.mli
@@ -23,5 +23,5 @@
  * http://helm.cs.unibo.it/
  *)
 
-val to_string: exn -> Token.flocation option * string
+val to_string: exn -> Stdpp.location option * string
 

diff --git a/matita/matitaGtkMisc.mli b/matita/matitaGtkMisc.mli
index 40fc9373bd68f7fd4aadb7dc757228af8235f640..0f78a4a61b45eadaa1a4cfe51e12e75ee9405765 100644 (file)
--- a/matita/matitaGtkMisc.mli
+++ b/matita/matitaGtkMisc.mli
@@ -146,7 +146,7 @@ val report_error:
 
     (* given an utf8 string a floc returns the parsed substring and its length
      * in bytes *)
-val utf8_parsed_text: string -> Token.flocation -> string * int
+val utf8_parsed_text: string -> Stdpp.location -> string * int
 
     (* the length in characters, not bytes *)
 val utf8_string_length: string -> int