]> matita.cs.unibo.it Git - helm.git/commitdiff
Porting to ocaml 5
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 30 Dec 2022 01:19:16 +0000 (02:19 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Feb 2023 14:22:45 +0000 (15:22 +0100)
- old hashing dropped from ocaml code => hash.c is not part of ng_paramodulation
- as a consequence, bytecode is now compile in -custom mode
- requires patched versions of ocaml-expant, ocamlnet and ulex-camlp5
  (all currently not accepted upstream yet)
- plenty of new warnings either turned off or applied to code
- ported to most recent version of camlp5

74 files changed:
matita/components/METAS/meta.helm-ng_paramodulation.src
matita/components/METAS/meta.helm-thread.src
matita/components/METAS/meta.helm-xml.src
matita/components/Makefile.common
matita/components/binaries/matitaprover/matitaprover.ml
matita/components/content/.depend.opt
matita/components/content_pres/.depend.opt
matita/components/content_pres/cicNotationParser.ml
matita/components/disambiguation/.depend.opt
matita/components/disambiguation/disambiguateTypes.ml
matita/components/extlib/.depend.opt
matita/components/extlib/patternMatcher.ml
matita/components/getter/.depend.opt
matita/components/getter/http_getter_misc.ml
matita/components/getter/http_getter_storage.ml
matita/components/grafite/.depend.opt
matita/components/grafite_engine/.depend.opt
matita/components/grafite_parser/.depend.opt
matita/components/grafite_parser/print_grammar.ml
matita/components/library/.depend.opt
matita/components/library/libraryClean.ml
matita/components/logger/.depend.opt
matita/components/ng_cic_content/.depend.opt
matita/components/ng_cic_content/interpretations.ml
matita/components/ng_disambiguation/.depend.opt
matita/components/ng_disambiguation/nCicDisambiguate.ml
matita/components/ng_extraction/.depend.opt
matita/components/ng_kernel/.depend.opt
matita/components/ng_kernel/nCicReduction.ml
matita/components/ng_kernel/nCicUntrusted.ml
matita/components/ng_kernel/nReference.ml
matita/components/ng_library/.depend.opt
matita/components/ng_paramodulation/.depend.opt
matita/components/ng_paramodulation/Makefile
matita/components/ng_paramodulation/foUtils.ml
matita/components/ng_paramodulation/hash.c [new file with mode: 0644]
matita/components/ng_paramodulation/index.ml
matita/components/ng_paramodulation/nCicBlob.ml
matita/components/ng_paramodulation/orderings.ml
matita/components/ng_paramodulation/stats.ml
matita/components/ng_paramodulation/terms.ml
matita/components/ng_refiner/.depend.opt
matita/components/ng_refiner/nCicCoercion.ml
matita/components/ng_refiner/nCicUnifHint.ml
matita/components/ng_refiner/nCicUnification.ml
matita/components/ng_refiner/nDiscriminationTree.ml
matita/components/ng_tactics/.depend.opt
matita/components/ng_tactics/nTacStatus.ml
matita/components/ng_tactics/nnAuto.ml
matita/components/registry/.depend.opt
matita/components/registry/helm_registry.ml
matita/components/syntax_extensions/.depend
matita/components/syntax_extensions/.depend.opt
matita/components/syntax_extensions/Makefile
matita/components/syntax_extensions/utf8Macro.ml
matita/components/syntax_extensions/utf8MacroTable.mli [new file with mode: 0644]
matita/components/thread/.depend.opt
matita/components/thread/extThread.ml
matita/components/xml/.depend.opt
matita/configure.ac
matita/matita/.depend.opt
matita/matita/Makefile
matita/matita/cicMathView.ml
matita/matita/contribs/lambdadelta/bin/recomm/mrcInput.ml
matita/matita/matitaExcPp.ml
matita/matita/matitaGtkMisc.mli
matita/matita/matitaGui.ml
matita/matita/matitaInit.ml
matita/matita/matitaMathView.ml
matita/matita/matitaMathView.mli
matita/matita/matitaMisc.ml
matita/matita/matitaMisc.mli
matita/matita/matitaScript.ml
matita/matita/predefined_virtuals.ml

index e09fa226a79fdbdb7e61d3bf969fc57eb6718eb4..01d35b82913281a85083d7af68c78c02d72850ca 100644 (file)
@@ -1,5 +1,5 @@
 requires="helm-ng_refiner"
 version="0.0.1"
-archive(byte)="ng_paramodulation.cma"
-archive(native)="ng_paramodulation.cmxa"
-linkopts=""
+archive(byte)="ng_paramodulation.cma hash.o"
+archive(native)="ng_paramodulation.cmxa hash.o"
+linkopts(byte)="-custom"
index 5253060d2202796a7a00843df883d605278806c2..8ee48782a4e4cfb19f44d8bb8c351cecb891573d 100644 (file)
@@ -1,4 +1,4 @@
-requires=""
+requires="str unix"
 version="0.0.1"
 archive(byte,mt)="thread.cma"
 archive(native,mt)="thread.cmxa"
index 626e644fcf14e5dba0c9ffe6c126b3fc173259ab..5cde1bdb8769c1d50365fda08cdf6c1f5d785833 100644 (file)
@@ -1,4 +1,4 @@
-requires="zip expat helm-extlib"
+requires="zip expat helm-extlib camlp-streams"
 version="0.0.1"
 archive(byte)="xml.cma"
 archive(native)="xml.cmxa"
index 74a54a821a07a686077a04caa180e20610ab5de4..0c61faaf763c8436a14eeb72ce93ab41eae9fcbb 100644 (file)
@@ -20,7 +20,7 @@ endif
 PREPROCOPTIONS = -pp camlp5o
 SYNTAXOPTIONS = -syntax camlp5o
 PREREQ =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3 # -57-3 for ocaml 4.0.5
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3-68-69-70 # -57-3 for ocaml 4.0.5, -68-69-70 for ocaml 5.0
 OCAMLDEBUGOPTIONS = -g
 #OCAML_PROF=p -p a
 OCAMLARCHIVEOPTIONS =
index f72a7ebc5c2520b6217d61f851fba79e96c1e89f..5e773bd09ccc1effe38d674366ede792160eaf3b 100644 (file)
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-module OT = struct type t = string  let compare = Pervasives.compare end 
+module OT = struct type t = string  let compare = Stdlib.compare end 
 module HC = Map.Make(OT)
 module TS = HTopoSort.Make(OT)
 
@@ -159,7 +159,7 @@ end
 
  let compute_stats goal hypotheses =
    let module C = 
-     struct type t = leaf let cmp (a,_) (b,_) = Pervasives.compare a b end 
+     struct type t = leaf let cmp (a,_) (b,_) = Stdlib.compare a b end 
    in
    let module B = MakeBlob(C) in
    let module Pp = Pp.Pp(B) in
@@ -189,8 +189,8 @@ end
         if a1 = 0 && a2 = 0 then 0
         else if a1 = 0 then -1
         else if a2 = 0 then 1
-        else let res = Pervasives.compare (a1,o1,-go1,p1) (a2,o2,-go2,p2)
-             in if res = 0 then Pervasives.compare (HExtlib.list_index ((=) n1) oplist) (HExtlib.list_index ((=) n2) oplist)
+        else let res = Stdlib.compare (a1,o1,-go1,p1) (a2,o2,-go2,p2)
+             in if res = 0 then Stdlib.compare (HExtlib.list_index ((=) n1) oplist) (HExtlib.list_index ((=) n2) oplist)
                 else res)
      data
  ;;
@@ -211,12 +211,12 @@ let worker order ~useage ~printmsg goal hypotheses =
         then
           ((*prerr_endline "NO CLASH, using fixed ground order";*)
            fun a b ->
-            Pervasives.compare 
+            Stdlib.compare 
               (pos a stats)
               (pos b stats))
         else
           ((*prerr_endline "CLASH, statistics insufficient";*)
-            fun (a,_) (b,_) -> Pervasives.compare a b)
+            fun (a,_) (b,_) -> Stdlib.compare a b)
       ;;
      end
    in
index 9c0b365c6a3ee363406a84761e14ee85ce710069..4ef84ec5d41f3dbd11d885ababb67d5a8a85fd42 100644 (file)
@@ -1,9 +1,22 @@
-content.cmx : content.cmi
+content.cmx : \
+    content.cmi
 content.cmi :
-notationEnv.cmx : notationUtil.cmx notationPt.cmx notationEnv.cmi
-notationEnv.cmi : notationPt.cmx
-notationPp.cmx : notationPt.cmx notationEnv.cmx notationPp.cmi
-notationPp.cmi : notationPt.cmx notationEnv.cmi
+notationEnv.cmx : \
+    notationUtil.cmx \
+    notationPt.cmx \
+    notationEnv.cmi
+notationEnv.cmi : \
+    notationPt.cmx
+notationPp.cmx : \
+    notationPt.cmx \
+    notationEnv.cmx \
+    notationPp.cmi
+notationPp.cmi : \
+    notationPt.cmx \
+    notationEnv.cmi
 notationPt.cmx :
-notationUtil.cmx : notationPt.cmx notationUtil.cmi
-notationUtil.cmi : notationPt.cmx
+notationUtil.cmx : \
+    notationPt.cmx \
+    notationUtil.cmi
+notationUtil.cmi : \
+    notationPt.cmx
index 211b4fc51200e2b3cf63db3bf38852b77c370dda..1e74dfbf4eeb81711b4dee2f3799a89da30564c5 100644 (file)
@@ -1,24 +1,55 @@
-box.cmx : renderingAttrs.cmx box.cmi
+box.cmx : \
+    renderingAttrs.cmx \
+    box.cmi
 box.cmi :
-boxPp.cmx : renderingAttrs.cmx mpresentation.cmx cicNotationPres.cmx box.cmx \
+boxPp.cmx : \
+    renderingAttrs.cmx \
+    mpresentation.cmx \
+    cicNotationPres.cmx \
+    box.cmx \
     boxPp.cmi
-boxPp.cmi : mpresentation.cmi cicNotationPres.cmi box.cmi
-cicNotationLexer.cmx : cicNotationLexer.cmi
+boxPp.cmi : \
+    mpresentation.cmi \
+    cicNotationPres.cmi \
+    box.cmi
+cicNotationLexer.cmx : \
+    cicNotationLexer.cmi
 cicNotationLexer.cmi :
-cicNotationParser.cmx : cicNotationLexer.cmx cicNotationParser.cmi
+cicNotationParser.cmx : \
+    cicNotationLexer.cmx \
+    cicNotationParser.cmi
 cicNotationParser.cmi :
-cicNotationPres.cmx : renderingAttrs.cmx mpresentation.cmx box.cmx \
+cicNotationPres.cmx : \
+    renderingAttrs.cmx \
+    mpresentation.cmx \
+    box.cmx \
     cicNotationPres.cmi
-cicNotationPres.cmi : mpresentation.cmi box.cmi
-content2pres.cmx : termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \
-    cicNotationPres.cmx box.cmx content2pres.cmi
-content2pres.cmi : termContentPres.cmi cicNotationPres.cmi
-content2presMatcher.cmx : content2presMatcher.cmi
+cicNotationPres.cmi : \
+    mpresentation.cmi \
+    box.cmi
+content2pres.cmx : \
+    termContentPres.cmx \
+    renderingAttrs.cmx \
+    mpresentation.cmx \
+    cicNotationPres.cmx \
+    box.cmx \
+    content2pres.cmi
+content2pres.cmi : \
+    termContentPres.cmi \
+    cicNotationPres.cmi
+content2presMatcher.cmx : \
+    content2presMatcher.cmi
 content2presMatcher.cmi :
-mpresentation.cmx : mpresentation.cmi
+mpresentation.cmx : \
+    mpresentation.cmi
 mpresentation.cmi :
-renderingAttrs.cmx : renderingAttrs.cmi
+renderingAttrs.cmx : \
+    renderingAttrs.cmi
 renderingAttrs.cmi :
-termContentPres.cmx : renderingAttrs.cmx content2presMatcher.cmx \
-    cicNotationParser.cmx termContentPres.cmi
-termContentPres.cmi : cicNotationParser.cmi
+termContentPres.cmx : \
+    renderingAttrs.cmx \
+    content2presMatcher.cmx \
+    cicNotationParser.cmx \
+    termContentPres.cmi
+termContentPres.cmi : \
+    cicNotationParser.cmi
index 3341b0febfea9fa55a2e96f0a889918dca41a8db..36a3fb01771bac4cfb10274087a1785dbd5b0741 100644 (file)
@@ -36,6 +36,11 @@ exception Level_not_found of int
 let min_precedence = 0
 let max_precedence = 100
 
+let hash_expr e =
+ e
+ |> Hashtbl.hash
+ |> Printf.sprintf "%08x"
+
 type ('a,'b,'c,'d,'e) grammars = {
   level1_pattern: 'a Grammar.Entry.e;
   level2_ast: 'b Grammar.Entry.e;
@@ -74,7 +79,7 @@ type db = {
 
 let int_of_string s =
   try
-    Pervasives.int_of_string s
+    Stdlib.int_of_string s
   with Failure _ ->
     failwith (sprintf "Lexer failure: string_of_int \"%s\" failed" s)
 
@@ -197,7 +202,8 @@ let extract_term_production status pattern =
         in
         [ Env (List.map Env.opt_declaration p_names),
           Gramext.srules
-            [ [ Gramext.Sopt (Gramext.srules [ p_atoms, p_action ]) ],
+            [ [ Gramext.Sopt (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ],
+              hash_expr action,
               Gramext.action action ] ]
     | Ast.List0 (p, _)
     | Ast.List1 (p, _) ->
@@ -215,7 +221,8 @@ let extract_term_production status pattern =
         in
         [ Env (List.map Env.list_declaration p_names),
           Gramext.srules
-            [ [ gram_of_list (Gramext.srules [ p_atoms, p_action ]) ],
+            [ [ gram_of_list (Gramext.srules [ p_atoms, hash_expr p_action, p_action ]) ],
+              hash_expr action,
               Gramext.action action ] ]
     | _ -> assert false
   and aux_variable =
@@ -246,7 +253,7 @@ let compare_rule_id x y =
     | _,[] -> 1
     | ((s1::tl1) as x),((s2::tl2) as y) ->
         if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
-        else Pervasives.compare x y 
+        else Stdlib.compare x y 
   in
     aux (x,y)
 
@@ -384,7 +391,7 @@ let initialize_grammars grammars =
   in
   (* Needed since campl4 on "delete_rule" remove the precedence level if it gets
    * empty after the deletion. The lexer never generate the Stoken below. *)
-  let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], dummy_action ] in
+  let dummy_prod = [ [ Gramext.Stoken ("DUMMY", "") ], "DUMMY", dummy_action ] in
   let mk_level_list first last =
     let rec aux acc = function
       | i when i < first -> acc
@@ -862,6 +869,7 @@ let extend (status : #status) (CL1P (level1_pattern,precedence)) action =
         [ None,
           Some (*Gramext.NonA*) Gramext.NonA,
           [ p_atoms, 
+            hash_expr "(make_action (fun (env: NotationEnv.t) (loc: Ast.location) -> (action env loc)) p_bindings)",
             (make_action
               (fun (env: NotationEnv.t) (loc: Ast.location) ->
                 (action env loc))
index 1f1711ae7f14eaf50a6f86c6fc91f58a0c7ce4a1..867ae46667610f8424caeb58720f553dbf57a72e 100644 (file)
@@ -1,7 +1,15 @@
-disambiguate.cmx : disambiguateTypes.cmx disambiguate.cmi
-disambiguate.cmi : disambiguateTypes.cmi
-disambiguateTypes.cmx : disambiguateTypes.cmi
+disambiguate.cmx : \
+    disambiguateTypes.cmx \
+    disambiguate.cmi
+disambiguate.cmi : \
+    disambiguateTypes.cmi
+disambiguateTypes.cmx : \
+    disambiguateTypes.cmi
 disambiguateTypes.cmi :
-multiPassDisambiguator.cmx : disambiguateTypes.cmx disambiguate.cmx \
+multiPassDisambiguator.cmx : \
+    disambiguateTypes.cmx \
+    disambiguate.cmx \
     multiPassDisambiguator.cmi
-multiPassDisambiguator.cmi : disambiguateTypes.cmi disambiguate.cmi
+multiPassDisambiguator.cmi : \
+    disambiguateTypes.cmi \
+    disambiguate.cmi
index 19c16d1305e89c3fdb0b734f370438eed5af5d38..9c37fa36c91ba5aa30bfe648c5e7dddeff067ca3 100644 (file)
@@ -41,7 +41,7 @@ exception Invalid_choice of (Stdpp.location * string) Lazy.t
 module OrderedDomain =
   struct
     type t = domain_item
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end
 
 (* module Domain = Set.Make (OrderedDomain) *)
index 12de49274a4db6fba23ff7191d8503ed1e943560..72b64d1cf2057a1003a71e5c1701c6dd31553614 100644 (file)
@@ -1,18 +1,30 @@
-componentsConf.cmx : componentsConf.cmi
+componentsConf.cmx : \
+    componentsConf.cmi
 componentsConf.cmi :
-discrimination_tree.cmx : trie.cmx hExtlib.cmx discrimination_tree.cmi
+discrimination_tree.cmx : \
+    trie.cmx \
+    hExtlib.cmx \
+    discrimination_tree.cmi
 discrimination_tree.cmi :
-graphvizPp.cmx : graphvizPp.cmi
+graphvizPp.cmx : \
+    graphvizPp.cmi
 graphvizPp.cmi :
-hExtlib.cmx : hExtlib.cmi
+hExtlib.cmx : \
+    hExtlib.cmi
 hExtlib.cmi :
-hLog.cmx : hLog.cmi
+hLog.cmx : \
+    hLog.cmi
 hLog.cmi :
-hMarshal.cmx : hExtlib.cmx hMarshal.cmi
+hMarshal.cmx : \
+    hExtlib.cmx \
+    hMarshal.cmi
 hMarshal.cmi :
-hTopoSort.cmx : hTopoSort.cmi
+hTopoSort.cmx : \
+    hTopoSort.cmi
 hTopoSort.cmi :
-patternMatcher.cmx : patternMatcher.cmi
+patternMatcher.cmx : \
+    patternMatcher.cmi
 patternMatcher.cmi :
-trie.cmx : trie.cmi
+trie.cmx : \
+    trie.cmi
 trie.cmi :
index fa8c6061ecc92ecbf767b7fef39e651a8aece27a..4e3e75fa560234aca5d7577219b0df9775e08b22 100644 (file)
@@ -33,7 +33,7 @@ type pattern_id = int
 module OrderedInt =
 struct
   type t = int
-  let compare (x1:t) (x2:t) = Pervasives.compare x2 x1  (* reverse order *)
+  let compare (x1:t) (x2:t) = Stdlib.compare x2 x1  (* reverse order *)
 end
 
 module IntSet = Set.Make (OrderedInt)
index 1d016d277ad431861b42fafb78ffdd2011480674..cb0f289acf8e0d744a5c22d63359ff7223571004 100644 (file)
@@ -1,23 +1,50 @@
-http_getter.cmx : http_getter_wget.cmx http_getter_types.cmx \
-    http_getter_storage.cmx http_getter_misc.cmx http_getter_logger.cmx \
-    http_getter_env.cmx http_getter_const.cmx http_getter_common.cmx \
+http_getter.cmx : \
+    http_getter_wget.cmx \
+    http_getter_types.cmx \
+    http_getter_storage.cmx \
+    http_getter_misc.cmx \
+    http_getter_logger.cmx \
+    http_getter_env.cmx \
+    http_getter_const.cmx \
+    http_getter_common.cmx \
     http_getter.cmi
-http_getter.cmi : http_getter_types.cmx
-http_getter_common.cmx : http_getter_types.cmx http_getter_misc.cmx \
-    http_getter_logger.cmx http_getter_env.cmx http_getter_common.cmi
-http_getter_common.cmi : http_getter_types.cmx
-http_getter_const.cmx : http_getter_const.cmi
+http_getter.cmi : \
+    http_getter_types.cmx
+http_getter_common.cmx : \
+    http_getter_types.cmx \
+    http_getter_misc.cmx \
+    http_getter_logger.cmx \
+    http_getter_env.cmx \
+    http_getter_common.cmi
+http_getter_common.cmi : \
+    http_getter_types.cmx
+http_getter_const.cmx : \
+    http_getter_const.cmi
 http_getter_const.cmi :
-http_getter_env.cmx : http_getter_types.cmx http_getter_misc.cmx \
-    http_getter_logger.cmx http_getter_const.cmx http_getter_env.cmi
-http_getter_env.cmi : http_getter_types.cmx
-http_getter_logger.cmx : http_getter_logger.cmi
+http_getter_env.cmx : \
+    http_getter_types.cmx \
+    http_getter_misc.cmx \
+    http_getter_logger.cmx \
+    http_getter_const.cmx \
+    http_getter_env.cmi
+http_getter_env.cmi : \
+    http_getter_types.cmx
+http_getter_logger.cmx : \
+    http_getter_logger.cmi
 http_getter_logger.cmi :
-http_getter_misc.cmx : http_getter_logger.cmx http_getter_misc.cmi
+http_getter_misc.cmx : \
+    http_getter_logger.cmx \
+    http_getter_misc.cmi
 http_getter_misc.cmi :
-http_getter_storage.cmx : http_getter_wget.cmx http_getter_types.cmx \
-    http_getter_misc.cmx http_getter_env.cmx http_getter_storage.cmi
+http_getter_storage.cmx : \
+    http_getter_wget.cmx \
+    http_getter_types.cmx \
+    http_getter_misc.cmx \
+    http_getter_env.cmx \
+    http_getter_storage.cmi
 http_getter_storage.cmi :
 http_getter_types.cmx :
-http_getter_wget.cmx : http_getter_types.cmx http_getter_wget.cmi
+http_getter_wget.cmx : \
+    http_getter_types.cmx \
+    http_getter_wget.cmi
 http_getter_wget.cmi :
index 38a943bc59b90091b89b32f6132b11c99ce427c5..fa5d780b07be470bdfc1cb729375bfea09e82568 100644 (file)
@@ -183,7 +183,7 @@ let gunzip ?(keep = false) ?output fname =
       (try
         while true do
           let bytes = Gzip.input ic buf 0 bufsiz in
-          if bytes = 0 then raise End_of_file else Pervasives.output oc buf 0 bytes
+          if bytes = 0 then raise End_of_file else Stdlib.output oc buf 0 bytes
         done
       with End_of_file -> ());
        close_out oc;
index 4ff552a4bf77ceea7f44520bd9a5b353028c16f0..be5cad2a9a579acee141a498546fa860e6c18f83 100644 (file)
@@ -70,7 +70,7 @@ let normalize_root uri =  (* add trailing slash to roots *)
   with Invalid_argument _ -> uri
 
 let remove_duplicates l =
-  Http_getter_misc.list_uniq (List.stable_sort Pervasives.compare l)
+  Http_getter_misc.list_uniq (List.stable_sort Stdlib.compare l)
 
 let has_rdonly l =  List.exists ((=) `Read_only) l
 let has_legacy l =  List.exists ((=) `Legacy) l
index 5dabb8012003194da1d473cc5a561e1d99bf65d2..be6de9f620c2921d2fe4f76ef368a0d4050c712f 100644 (file)
@@ -1,3 +1,6 @@
 grafiteAst.cmx :
-grafiteAstPp.cmx : grafiteAst.cmx grafiteAstPp.cmi
-grafiteAstPp.cmi : grafiteAst.cmx
+grafiteAstPp.cmx : \
+    grafiteAst.cmx \
+    grafiteAstPp.cmi
+grafiteAstPp.cmi : \
+    grafiteAst.cmx
index 696b4588179e989a2ae83a739c57852e3d51d8f6..6e9ccb21aa298feaf832ca1ec51706dd0ae0fcde 100644 (file)
@@ -1,7 +1,14 @@
-grafiteEngine.cmx : nCicCoercDeclaration.cmx grafiteTypes.cmx \
+grafiteEngine.cmx : \
+    nCicCoercDeclaration.cmx \
+    grafiteTypes.cmx \
     grafiteEngine.cmi
-grafiteEngine.cmi : grafiteTypes.cmi
-grafiteTypes.cmx : grafiteTypes.cmi
+grafiteEngine.cmi : \
+    grafiteTypes.cmi
+grafiteTypes.cmx : \
+    grafiteTypes.cmi
 grafiteTypes.cmi :
-nCicCoercDeclaration.cmx : grafiteTypes.cmx nCicCoercDeclaration.cmi
-nCicCoercDeclaration.cmi : grafiteTypes.cmi
+nCicCoercDeclaration.cmx : \
+    grafiteTypes.cmx \
+    nCicCoercDeclaration.cmi
+nCicCoercDeclaration.cmi : \
+    grafiteTypes.cmi
index e0e6dac9c2dcb31f52f80b9b237789c528f048cf..4b014236d6d2f86ed97fc75ebd600632dc5d3004 100644 (file)
@@ -1,4 +1,7 @@
-grafiteParser.cmx : grafiteParser.cmi
+grafiteParser.cmx : \
+    grafiteParser.cmi
 grafiteParser.cmi :
-print_grammar.cmx : print_grammar.cmi
-print_grammar.cmi : grafiteParser.cmi
+print_grammar.cmx : \
+    print_grammar.cmi
+print_grammar.cmi : \
+    grafiteParser.cmi
index 9fea12e40fbd9ceda710866d0862757f3df1e396..9951402820b473f2758d798145af2ec3a1c2a412 100644 (file)
@@ -84,7 +84,6 @@ and is_entry_dummy = function
 and is_symbol_dummy = function
   | Stoken ("DUMMY", _) -> true
   | Stoken _ -> false
-  | Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
   | Snterm e | Snterml (e, _) -> is_entry_dummy e
   | Slist1 x | Slist0 x -> is_symbol_dummy x
   | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y
@@ -170,15 +169,6 @@ let visit_description desc fmt self =
     
   and visit_symbol s todo is_son  =
     match s with
-    | Smeta (name, sl, _) -> 
-        Format.fprintf fmt "%s " name;
-        List.fold_left (
-          fun acc s -> 
-            let todo = visit_symbol s acc is_son  in
-            if is_son then
-              Format.fprintf fmt "@ ";
-            todo) 
-        todo sl
     | Snterm entry -> visit_entry entry todo is_son  
     | Snterml (entry,level) -> visit_entry entry ~level todo is_son 
     | Slist0 symbol -> 
@@ -256,7 +246,7 @@ let rec visit_entries fmt todo pped =
           ~eq:(fun e1 e2 -> (name_of_entry e1) = (name_of_entry e2))
           (List.sort 
             (fun e1 e2 -> 
-              Pervasives.compare (name_of_entry e1) (name_of_entry e2))
+              Stdlib.compare (name_of_entry e1) (name_of_entry e2))
             todo),
         pped
       in
index 27ecf93835014baa578b3cd07a7cb09b8cb5a687..d960dc9be94174149284cd7bba2b3c24c47f5006 100644 (file)
@@ -1,6 +1,9 @@
-librarian.cmx : librarian.cmi
+librarian.cmx : \
+    librarian.cmi
 librarian.cmi :
-libraryClean.cmx : libraryClean.cmi
+libraryClean.cmx : \
+    libraryClean.cmi
 libraryClean.cmi :
-libraryMisc.cmx : libraryMisc.cmi
+libraryMisc.cmx : \
+    libraryMisc.cmi
 libraryMisc.cmi :
index 1b3df75f8e89011a3affc7e3a80e80011e193713..ebd02bd1bc4f9e5e1352b24f73acc45e08e13224 100644 (file)
@@ -85,7 +85,7 @@ let one_step_depend cache_of_processed_baseuri suri dbtype dbd =
                 Filename.dirname (strip_xpointer occ) = buri -> 
                   l := uri :: !l
             | _ -> ());
-        let l = List.sort Pervasives.compare !l in
+        let l = List.sort Stdlib.compare !l in
         HExtlib.list_uniq l
       with
         exn -> raise exn (* no errors should be accepted *)
@@ -120,7 +120,7 @@ let db_uris_of_baseuri buri =
       | Some uri when Filename.dirname (strip_xpointer uri) = buri -> 
           l := uri :: !l
       | _ -> ());
-  let l = List.sort Pervasives.compare !l in
+  let l = List.sort Stdlib.compare !l in
   HExtlib.list_uniq l
  with
   exn -> raise exn (* no errors should be accepted *)
@@ -135,7 +135,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove =
   (* to remove an uri you have to remove the whole script *)
   let buri_to_remove = 
     HExtlib.list_uniq 
-      (List.fast_sort Pervasives.compare 
+      (List.fast_sort Stdlib.compare 
         (List.map safe_buri_of_suri uri_to_remove))
   in
   (* cleand the already visided baseuris *)
@@ -177,7 +177,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove =
   in
   let uri_to_remove = uri_to_remove @ uri_to_remove_from_db in
   let uri_to_remove =
-   HExtlib.list_uniq (List.sort Pervasives.compare uri_to_remove) in
+   HExtlib.list_uniq (List.sort Stdlib.compare uri_to_remove) in
   (* now we want the list of all uri that depend on them *) 
   let depend = 
     List.fold_left
@@ -185,7 +185,7 @@ let close_uri_list cache_of_processed_baseuri uri_to_remove =
     [] uri_to_remove
   in
   let depend = 
-    HExtlib.list_uniq (List.fast_sort Pervasives.compare depend) 
+    HExtlib.list_uniq (List.fast_sort Stdlib.compare depend) 
   in
   uri_to_remove, depend
 ;;
@@ -229,7 +229,7 @@ let clean_baseuris ?verbose:(_=true) _buris =
   if debug then
     List.iter debug_prerr buris; 
   let l = close_db cache_of_processed_baseuri [] buris in
-  let l = HExtlib.list_uniq (List.fast_sort Pervasives.compare l) in
+  let l = HExtlib.list_uniq (List.fast_sort Stdlib.compare l) in
   let l = List.map NUri.uri_of_string l in
   debug_prerr "clean_baseuri will remove:";
   if debug then
@@ -245,6 +245,6 @@ let clean_baseuris ?verbose:(_=true) _buris =
        HExtlib.safe_remove lexiconfile;
        HExtlib.rmdir_descend (Filename.chop_extension lexiconfile)
      with Http_getter_types.Key_not_found _ -> ())
-   (HExtlib.list_uniq (List.fast_sort Pervasives.compare
+   (HExtlib.list_uniq (List.fast_sort Stdlib.compare
      (List.map NUri.baseuri_of_uri l @ buris)))
 *)
index ed934897fdbd39b817c5b6303e596f74dff221d2..f68fdd43edd08bca296439c4e75855fdc1bcf174 100644 (file)
@@ -1,2 +1,3 @@
-helmLogger.cmx : helmLogger.cmi
+helmLogger.cmx : \
+    helmLogger.cmi
 helmLogger.cmi :
index df8d6d6357841ca9eecfae3246d3df739c1c1f16..b526a0df50c27c55e8a8cca227e75fc1308f069b 100644 (file)
@@ -1,4 +1,7 @@
-interpretations.cmx : ncic2astMatcher.cmx interpretations.cmi
+interpretations.cmx : \
+    ncic2astMatcher.cmx \
+    interpretations.cmi
 interpretations.cmi :
-ncic2astMatcher.cmx : ncic2astMatcher.cmi
+ncic2astMatcher.cmx : \
+    ncic2astMatcher.cmi
 ncic2astMatcher.cmi :
index 794859369bbc62f593f392b80b73fcf63d6e19b7..44d7751d500d74232d482a0e5117ddce72a6d066 100644 (file)
@@ -38,10 +38,12 @@ let hide_coercions = ref true;;
 
 type cic_id = string
 
+(*
 type term_info =
   { sort: (cic_id, Ast.sort_kind) Hashtbl.t;
     uri: (cic_id, NReference.reference) Hashtbl.t;
   }
+*)
 
 module IntMap = Map.Make(struct type t = int let compare = compare end);;
 module StringMap = Map.Make(String);;
@@ -185,7 +187,7 @@ let lookup_interpretations status ?(sorted=true) symbol =
           dsc, args, appl_pattern
       ) (StringMap.find symbol status#interp_db.interpretations)
     in
-    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+    if sorted then HExtlib.list_uniq (List.sort Stdlib.compare raw)
               else raw
   with Not_found -> raise Interpretation_not_found
 
index d5eef6bc06265d73f5d3443041b60c587a92931f..6904cfd3b7d85bf4f66651ac11acaf57ff2c8316 100644 (file)
@@ -1,9 +1,15 @@
-disambiguateChoices.cmx : nnumber_notation.cmx disambiguateChoices.cmi
+disambiguateChoices.cmx : \
+    nnumber_notation.cmx \
+    disambiguateChoices.cmi
 disambiguateChoices.cmi :
-grafiteDisambiguate.cmx : nCicDisambiguate.cmx disambiguateChoices.cmx \
+grafiteDisambiguate.cmx : \
+    nCicDisambiguate.cmx \
+    disambiguateChoices.cmx \
     grafiteDisambiguate.cmi
 grafiteDisambiguate.cmi :
-nCicDisambiguate.cmx : nCicDisambiguate.cmi
+nCicDisambiguate.cmx : \
+    nCicDisambiguate.cmi
 nCicDisambiguate.cmi :
-nnumber_notation.cmx : nnumber_notation.cmi
+nnumber_notation.cmx : \
+    nnumber_notation.cmi
 nnumber_notation.cmi :
index 59fe713e560d989766209f4d3a55b066bd92a335..8ed903be16be436e09a4da2f61326fc562103040 100644 (file)
@@ -103,7 +103,7 @@ let find_in_context name context =
   aux 1 context
 
 let interpretate_term_and_interpretate_term_option (status: #NCic.status)
-  ?(create_dummy_ids=false) ~obj_context ~mk_choice ~env ~uri ~is_path
+  ~create_dummy_ids ~obj_context ~mk_choice ~env ~uri ~is_path
   ~localization_tbl 
 =
   (* create_dummy_ids shouldbe used only for interpretating patterns *)
index 3b0b9b57c0b4764f81aa8fd6ac7cd4ae3161a6fc..a527ad0c4373fc9b2607c35b35e70e5d17d2d13e 100644 (file)
@@ -1,20 +1,61 @@
-common.cmx : ocamlExtractionTable.cmx mlutil.cmx coq.cmx common.cmi
-common.cmi : ocamlExtractionTable.cmi coq.cmi
-coq.cmx : coq.cmi
+common.cmx : \
+    ocamlExtractionTable.cmx \
+    mlutil.cmx \
+    coq.cmx \
+    common.cmi
+common.cmi : \
+    ocamlExtractionTable.cmi \
+    coq.cmi
+coq.cmx : \
+    coq.cmi
 coq.cmi :
-extraction.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
-    common.cmx extraction.cmi
-extraction.cmi : ocamlExtractionTable.cmi miniml.cmx
-miniml.cmx : coq.cmx
-mlutil.cmx : ocamlExtractionTable.cmx miniml.cmx coq.cmx mlutil.cmi
-mlutil.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-nCicExtraction.cmx : nCicExtraction.cmi
+extraction.cmx : \
+    ocamlExtractionTable.cmx \
+    mlutil.cmx \
+    miniml.cmx \
+    coq.cmx \
+    common.cmx \
+    extraction.cmi
+extraction.cmi : \
+    ocamlExtractionTable.cmi \
+    miniml.cmx
+miniml.cmx : \
+    coq.cmx
+mlutil.cmx : \
+    ocamlExtractionTable.cmx \
+    miniml.cmx \
+    coq.cmx \
+    mlutil.cmi
+mlutil.cmi : \
+    ocamlExtractionTable.cmi \
+    miniml.cmx \
+    coq.cmi
+nCicExtraction.cmx : \
+    nCicExtraction.cmi
 nCicExtraction.cmi :
-ocaml.cmx : ocamlExtractionTable.cmx mlutil.cmx miniml.cmx coq.cmx \
-    common.cmx ocaml.cmi
-ocaml.cmi : ocamlExtractionTable.cmi miniml.cmx coq.cmi
-ocamlExtraction.cmx : ocamlExtractionTable.cmx ocaml.cmx extraction.cmx \
-    coq.cmx ocamlExtraction.cmi
-ocamlExtraction.cmi : ocamlExtractionTable.cmi
-ocamlExtractionTable.cmx : miniml.cmx coq.cmx ocamlExtractionTable.cmi
-ocamlExtractionTable.cmi : miniml.cmx coq.cmi
+ocaml.cmx : \
+    ocamlExtractionTable.cmx \
+    mlutil.cmx \
+    miniml.cmx \
+    coq.cmx \
+    common.cmx \
+    ocaml.cmi
+ocaml.cmi : \
+    ocamlExtractionTable.cmi \
+    miniml.cmx \
+    coq.cmi
+ocamlExtraction.cmx : \
+    ocamlExtractionTable.cmx \
+    ocaml.cmx \
+    extraction.cmx \
+    coq.cmx \
+    ocamlExtraction.cmi
+ocamlExtraction.cmi : \
+    ocamlExtractionTable.cmi
+ocamlExtractionTable.cmx : \
+    miniml.cmx \
+    coq.cmx \
+    ocamlExtractionTable.cmi
+ocamlExtractionTable.cmi : \
+    miniml.cmx \
+    coq.cmi
index 97f4e283a4931b06831fb2f0a127550417b2f0b2..fe01e3cc1b04c3e6ea14e5e5f067272367855e2f 100644 (file)
@@ -1,24 +1,74 @@
-nCic.cmx : nUri.cmx nReference.cmx
-nCicEnvironment.cmx : nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi
-nCicEnvironment.cmi : nUri.cmi nReference.cmi nCic.cmx
-nCicPp.cmx : nUri.cmx nReference.cmx nCicSubstitution.cmx nCicReduction.cmx \
-    nCicEnvironment.cmx nCic.cmx nCicPp.cmi
-nCicPp.cmi : nReference.cmi nCic.cmx
-nCicReduction.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-    nCicEnvironment.cmx nCic.cmx nCicReduction.cmi
-nCicReduction.cmi : nCic.cmx
-nCicSubstitution.cmx : nCicUtils.cmx nCic.cmx nCicSubstitution.cmi
-nCicSubstitution.cmi : nCic.cmx
-nCicTypeChecker.cmx : nUri.cmx nReference.cmx nCicUtils.cmx \
-    nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \
+nCic.cmx : \
+    nUri.cmx \
+    nReference.cmx
+nCicEnvironment.cmx : \
+    nUri.cmx \
+    nReference.cmx \
+    nCic.cmx \
+    nCicEnvironment.cmi
+nCicEnvironment.cmi : \
+    nUri.cmi \
+    nReference.cmi \
+    nCic.cmx
+nCicPp.cmx : \
+    nUri.cmx \
+    nReference.cmx \
+    nCicSubstitution.cmx \
+    nCicReduction.cmx \
+    nCicEnvironment.cmx \
+    nCic.cmx \
+    nCicPp.cmi
+nCicPp.cmi : \
+    nReference.cmi \
+    nCic.cmx
+nCicReduction.cmx : \
+    nReference.cmx \
+    nCicUtils.cmx \
+    nCicSubstitution.cmx \
+    nCicEnvironment.cmx \
+    nCic.cmx \
+    nCicReduction.cmi
+nCicReduction.cmi : \
+    nCic.cmx
+nCicSubstitution.cmx : \
+    nCicUtils.cmx \
+    nCic.cmx \
+    nCicSubstitution.cmi
+nCicSubstitution.cmi : \
+    nCic.cmx
+nCicTypeChecker.cmx : \
+    nUri.cmx \
+    nReference.cmx \
+    nCicUtils.cmx \
+    nCicSubstitution.cmx \
+    nCicReduction.cmx \
+    nCicEnvironment.cmx \
+    nCic.cmx \
     nCicTypeChecker.cmi
-nCicTypeChecker.cmi : nUri.cmi nReference.cmi nCic.cmx
-nCicUntrusted.cmx : nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \
-    nCicReduction.cmx nCicEnvironment.cmx nCic.cmx nCicUntrusted.cmi
-nCicUntrusted.cmi : nCic.cmx
-nCicUtils.cmx : nCic.cmx nCicUtils.cmi
-nCicUtils.cmi : nCic.cmx
-nReference.cmx : nUri.cmx nReference.cmi
-nReference.cmi : nUri.cmi
-nUri.cmx : nUri.cmi
+nCicTypeChecker.cmi : \
+    nUri.cmi \
+    nReference.cmi \
+    nCic.cmx
+nCicUntrusted.cmx : \
+    nReference.cmx \
+    nCicUtils.cmx \
+    nCicSubstitution.cmx \
+    nCicReduction.cmx \
+    nCicEnvironment.cmx \
+    nCic.cmx \
+    nCicUntrusted.cmi
+nCicUntrusted.cmi : \
+    nCic.cmx
+nCicUtils.cmx : \
+    nCic.cmx \
+    nCicUtils.cmi
+nCicUtils.cmi : \
+    nCic.cmx
+nReference.cmx : \
+    nUri.cmx \
+    nReference.cmi
+nReference.cmi : \
+    nUri.cmi
+nUri.cmx : \
+    nUri.cmi
 nUri.cmi :
index 7542a52e03683ce1bb3905c3e6dc28fe7b7c2af9..9234f07aab85f9acf1d2fc5831b0743f7e7733cc 100644 (file)
@@ -206,7 +206,7 @@ module R = Reduction(RS);;
 
 let whd = R.whd
 
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
 
 let get_relevance = ref (fun _ ~metasenv:_ ~subst:_ _ _ -> assert false);;
 
index 5df06d28d001cdfbc0d74a84e15fbbc2f5f1b91c..e60bf7e504264c51ef5802f3f4d8057940aa715a 100644 (file)
@@ -69,7 +69,7 @@ let metas_of_term status subst context term =
             List.fold_left (aux ctx) (i::acc) l)
     | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
   in
-    HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
+    HExtlib.list_uniq (List.sort Stdlib.compare (aux context [] term))
 ;;
 
 module NCicHash =
@@ -282,7 +282,7 @@ let max_kind k1 k2 =
 module OT = 
   struct 
     type t = int * NCic.conjecture
-    let compare (i,_) (j,_) = Pervasives.compare i j
+    let compare (i,_) (j,_) = Stdlib.compare i j
   end
 
 module MS = HTopoSort.Make(OT)
index 102f25046f84187a495d5778deebf1f1c6148d5d..5fd28044dd872f179df5ba49ad32b14bf41bbb25 100644 (file)
@@ -37,7 +37,7 @@ let hash (Ref (uri,spec)) =
 module OrderedStrings =
  struct
   type t = string
-  let compare (s1 : t) (s2 : t) = Pervasives.compare s1 s2
+  let compare (s1 : t) (s2 : t) = Stdlib.compare s1 s2
  end
 ;;
 
index 07d53f5dd0b86ddb9d895e15e2c8914d08d5ceac..ee5e8bd16982af5acf6fbe05ccfef171d01c9879 100644 (file)
@@ -1,2 +1,3 @@
-nCicLibrary.cmx : nCicLibrary.cmi
+nCicLibrary.cmx : \
+    nCicLibrary.cmi
 nCicLibrary.cmi :
index 9593d8958d5a5c3006d2a1ae22910ad20895acb8..32cbf605dfb51beb762d0971269c0c1b56c1e5fc 100644 (file)
@@ -1,29 +1,98 @@
-foSubst.cmx : terms.cmx foSubst.cmi
-foSubst.cmi : terms.cmi
-foUnif.cmx : terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi
-foUnif.cmi : terms.cmi orderings.cmi
-foUtils.cmx : terms.cmx orderings.cmx foSubst.cmx foUtils.cmi
-foUtils.cmi : terms.cmi orderings.cmi
-index.cmx : terms.cmx orderings.cmx foUtils.cmx index.cmi
-index.cmi : terms.cmi orderings.cmi
-nCicBlob.cmx : terms.cmx foUtils.cmx nCicBlob.cmi
-nCicBlob.cmi : terms.cmi
-nCicParamod.cmx : terms.cmx pp.cmx paramod.cmx orderings.cmx nCicProof.cmx \
-    nCicBlob.cmx nCicParamod.cmi
-nCicParamod.cmi : terms.cmi
-nCicProof.cmx : terms.cmx pp.cmx nCicBlob.cmx foSubst.cmx nCicProof.cmi
-nCicProof.cmi : terms.cmi
-orderings.cmx : terms.cmx foSubst.cmx orderings.cmi
-orderings.cmi : terms.cmi
-paramod.cmx : terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
-    foUtils.cmx paramod.cmi
-paramod.cmi : terms.cmi orderings.cmi
-pp.cmx : terms.cmx pp.cmi
-pp.cmi : terms.cmi
-stats.cmx : terms.cmx stats.cmi
-stats.cmi : terms.cmi orderings.cmi
-superposition.cmx : terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
-    foUnif.cmx foSubst.cmx superposition.cmi
-superposition.cmi : terms.cmi orderings.cmi index.cmi
-terms.cmx : terms.cmi
+foSubst.cmx : \
+    terms.cmx \
+    foSubst.cmi
+foSubst.cmi : \
+    terms.cmi
+foUnif.cmx : \
+    terms.cmx \
+    orderings.cmx \
+    foUtils.cmx \
+    foSubst.cmx \
+    foUnif.cmi
+foUnif.cmi : \
+    terms.cmi \
+    orderings.cmi
+foUtils.cmx : \
+    terms.cmx \
+    orderings.cmx \
+    foSubst.cmx \
+    foUtils.cmi
+foUtils.cmi : \
+    terms.cmi \
+    orderings.cmi
+index.cmx : \
+    terms.cmx \
+    orderings.cmx \
+    foUtils.cmx \
+    index.cmi
+index.cmi : \
+    terms.cmi \
+    orderings.cmi
+nCicBlob.cmx : \
+    terms.cmx \
+    foUtils.cmx \
+    nCicBlob.cmi
+nCicBlob.cmi : \
+    terms.cmi
+nCicParamod.cmx : \
+    terms.cmx \
+    pp.cmx \
+    paramod.cmx \
+    orderings.cmx \
+    nCicProof.cmx \
+    nCicBlob.cmx \
+    nCicParamod.cmi
+nCicParamod.cmi : \
+    terms.cmi
+nCicProof.cmx : \
+    terms.cmx \
+    pp.cmx \
+    nCicBlob.cmx \
+    foSubst.cmx \
+    nCicProof.cmi
+nCicProof.cmi : \
+    terms.cmi
+orderings.cmx : \
+    terms.cmx \
+    foSubst.cmx \
+    orderings.cmi
+orderings.cmi : \
+    terms.cmi
+paramod.cmx : \
+    terms.cmx \
+    superposition.cmx \
+    pp.cmx \
+    orderings.cmx \
+    index.cmx \
+    foUtils.cmx \
+    paramod.cmi
+paramod.cmi : \
+    terms.cmi \
+    orderings.cmi
+pp.cmx : \
+    terms.cmx \
+    pp.cmi
+pp.cmi : \
+    terms.cmi
+stats.cmx : \
+    terms.cmx \
+    stats.cmi
+stats.cmi : \
+    terms.cmi \
+    orderings.cmi
+superposition.cmx : \
+    terms.cmx \
+    pp.cmx \
+    orderings.cmx \
+    index.cmx \
+    foUtils.cmx \
+    foUnif.cmx \
+    foSubst.cmx \
+    superposition.cmi
+superposition.cmi : \
+    terms.cmi \
+    orderings.cmi \
+    index.cmi
+terms.cmx : \
+    terms.cmi
 terms.cmi :
index f4c10223999a12ff38bcaeb7de2ea57ce73eff53..ca2e5d1af8d9664aad387ab428295afab5b91bd2 100644 (file)
@@ -8,7 +8,11 @@ INTERFACE_FILES = \
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
-all:
+all: hash.o
+opt: hash.o
+
+hash.o:
+       gcc -I `ocamlc -where`/caml/ -c hash.c
 
 include ../../Makefile.defs
 include ../Makefile.common
index 826687afc788b49d842b639d83467c94b88fd5de..9bb7891c382f6c375fdf7da9437a9ec9aadd01e0 100644 (file)
@@ -58,7 +58,7 @@ module Utils (B : Orderings.Blob) = struct
     match l1, l2 with
     | Terms.Predicate p1, Terms.Predicate p2 -> compare_foterm p1 p2
     | Terms.Equation (l1,r1,ty1,o1), Terms.Equation (l2,r2,ty2,o2) ->
-        let c = Pervasives.compare o1 o2 in
+        let c = Stdlib.compare o1 o2 in
         if c <> 0 then c else
           let c = compare_foterm l1 l2 in
           if c <> 0 then c else
@@ -70,7 +70,7 @@ module Utils (B : Orderings.Blob) = struct
   ;;
 
   let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2
-  let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2
+  let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Stdlib.compare id1 id2
     
   let relocate maxvar varlist subst =
     List.fold_right
diff --git a/matita/components/ng_paramodulation/hash.c b/matita/components/ng_paramodulation/hash.c
new file mode 100644 (file)
index 0000000..262c36e
--- /dev/null
@@ -0,0 +1,152 @@
+/***********************************************************************/
+/*                                                                     */
+/*                                OCaml                                */
+/*                                                                     */
+/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
+/*                                                                     */
+/*  Copyright 1996 Institut National de Recherche en Informatique et   */
+/*  en Automatique.  All rights reserved.  This file is distributed    */
+/*  under the terms of the GNU Library General Public License, with    */
+/*  the special exception on linking described in file ../LICENSE.     */
+/*                                                                     */
+/***********************************************************************/
+
+/* $Id: hash.c 12149 2012-02-10 16:15:24Z doligez $ */
+
+/* The generic hashing primitive */
+
+/* The interface of this file is in "mlvalues.h" (for [caml_hash_variant])
+   and in "hash.h" (for the other exported functions). */
+
+#include "mlvalues.h"
+#include "custom.h"
+#include "memory.h"
+#include "hash.h"
+#include "address_class.h"
+
+/*#ifdef ARCH_INT64_TYPE
+#include "int64_native.h"
+#else
+#include "int64_emul.h"
+#endif*/
+
+/* The old implementation */
+
+static uintnat hash_accu;
+static intnat hash_univ_limit, hash_univ_count;
+
+static void hash_aux(value obj);
+
+CAMLprim value caml_hash_univ_param(value count, value limit, value obj)
+{
+  hash_univ_limit = Long_val(limit);
+  hash_univ_count = Long_val(count);
+  hash_accu = 0;
+  hash_aux(obj);
+  return Val_long(hash_accu & 0x3FFFFFFF);
+  /* The & has two purposes: ensure that the return value is positive
+     and give the same result on 32 bit and 64 bit architectures. */
+}
+
+#define Alpha 65599
+#define Beta 19
+#define Combine(new)  (hash_accu = hash_accu * Alpha + (new))
+#define Combine_small(new) (hash_accu = hash_accu * Beta + (new))
+
+static void hash_aux(value obj)
+{
+  unsigned char * p;
+  mlsize_t i, j;
+  tag_t tag;
+
+  hash_univ_limit--;
+  if (hash_univ_count < 0 || hash_univ_limit < 0) return;
+
+ again:
+  if (Is_long(obj)) {
+    hash_univ_count--;
+    Combine(Long_val(obj));
+    return;
+  }
+
+  /* Pointers into the heap are well-structured blocks. So are atoms.
+     We can inspect the block contents. */
+
+  CAMLassert (Is_block (obj));
+  if (Is_in_value_area(obj)) {
+    tag = Tag_val(obj);
+    switch (tag) {
+    case String_tag:
+      hash_univ_count--;
+      i = caml_string_length(obj);
+      for (p = &Byte_u(obj, 0); i > 0; i--, p++)
+        Combine_small(*p);
+      break;
+    case Double_tag:
+      /* For doubles, we inspect their binary representation, LSB first.
+         The results are consistent among all platforms with IEEE floats. */
+      hash_univ_count--;
+#ifdef ARCH_BIG_ENDIAN
+      for (p = &Byte_u(obj, sizeof(double) - 1), i = sizeof(double);
+           i > 0;
+           p--, i--)
+#else
+      for (p = &Byte_u(obj, 0), i = sizeof(double);
+           i > 0;
+           p++, i--)
+#endif
+        Combine_small(*p);
+      break;
+    case Double_array_tag:
+      hash_univ_count--;
+      for (j = 0; j < Bosize_val(obj); j += sizeof(double)) {
+#ifdef ARCH_BIG_ENDIAN
+      for (p = &Byte_u(obj, j + sizeof(double) - 1), i = sizeof(double);
+           i > 0;
+           p--, i--)
+#else
+      for (p = &Byte_u(obj, j), i = sizeof(double);
+           i > 0;
+           p++, i--)
+#endif
+        Combine_small(*p);
+      }
+      break;
+    case Abstract_tag:
+      /* We don't know anything about the contents of the block.
+         Better do nothing. */
+      break;
+    case Infix_tag:
+      hash_aux(obj - Infix_offset_val(obj));
+      break;
+    case Forward_tag:
+      obj = Forward_val (obj);
+      goto again;
+    case Object_tag:
+      hash_univ_count--;
+      Combine(Oid_val(obj));
+      break;
+    case Custom_tag:
+      /* If no hashing function provided, do nothing */
+      if (Custom_ops_val(obj)->hash != NULL) {
+        hash_univ_count--;
+        Combine(Custom_ops_val(obj)->hash(obj));
+      }
+      break;
+    default:
+      hash_univ_count--;
+      Combine_small(tag);
+      i = Wosize_val(obj);
+      while (i != 0) {
+        i--;
+        hash_aux(Field(obj, i));
+      }
+      break;
+    }
+    return;
+  }
+
+  /* Otherwise, obj is a pointer outside the heap, to an object with
+     a priori unknown structure. Use its physical address as hash key. */
+  Combine((intnat) obj);
+}
index c1e12a34dbbc684c38560e2bae7ff046aff1eabf..fa5d86ee3e913cf14409b13e6c82bfbbc86c13d6 100644 (file)
@@ -21,7 +21,7 @@ module Index(B : Orderings.Blob) = struct
       type t = Terms.direction * B.t Terms.unit_clause
  
       let compare (d1,uc1) (d2,uc2) = 
-        let c = Pervasives.compare d1 d2 in
+        let c = Stdlib.compare d1 d2 in
         if c <> 0 then c else U.compare_unit_clause uc1 uc2
       ;;
     end
@@ -61,7 +61,7 @@ module Index(B : Orderings.Blob) = struct
         match e1,e2 with 
         | Constant (a1,ar1), Constant (a2,ar2) ->
             let c = B.compare a1 a2 in
-            if c <> 0 then c else Pervasives.compare ar1 ar2
+            if c <> 0 then c else Stdlib.compare ar1 ar2
         | Variable, Variable -> 0
         | Constant _, Variable -> ~-1
         | Variable, Constant _ -> 1
index b1f2cfa6f2d9cb4774a56c3e89862209759b8983..9ca541a65ca7afa4a48cfad6c7ee594cc9a5cbf0 100644 (file)
@@ -80,7 +80,7 @@ with type t = NCic.term and type input = NCic.term = struct
     | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1
     | NCic.Appl _, NCic.Meta _ -> ~-1
     | NCic.Meta _, NCic.Appl _ -> 1
-    | _ -> Pervasives.compare x y
+    | _ -> Stdlib.compare x y
        (* was assert false, but why? *)
        
   ;;
index d5f35a3a321c16929177d4af525239dfcac334dc..8da829e750df1e71daff86dde4b93b8cab9d1c4e 100644 (file)
@@ -130,7 +130,7 @@ let compare_weights (h1, w1) (h2, w2) =
       | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
           if var1 = var2 then
             let diffs = (w1 - w2) + diffs in
-            let r = Pervasives.compare w1 w2 in
+            let r = Stdlib.compare w1 w2 in
             let lt = lt || (r < 0) in
             let gt = gt || (r > 0) in
               if lt && gt then XINCOMPARABLE else
index da00eb5511145c02d99a9dce6aa924bf273ae737..a1e892902002f8d83f56067888633e3d4bb0a038 100644 (file)
@@ -129,7 +129,7 @@ module Stats (B : Terms.Blob) =
                    | _ -> dependencies op tl acc
     ;;
 
-    let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
+    let dependencies op clauses = HExtlib.list_uniq (List.sort Stdlib.compare (dependencies op clauses []));;
 
     (* let max_weight_hyp = *)
 
index 87b4f383bc53bf13885069592eaf896ad9f58a0e..0aa2a7d2bdfd401b721c3d847594d325fa041358 100644 (file)
@@ -63,7 +63,7 @@ let vars_of_term t =
 module OT =
  struct
    type t = int 
-   let compare = Pervasives.compare
+   let compare = Stdlib.compare
  end
 
 module M : Map.S with type key = int 
index dab8738901678689b5c7753b5a95b2e45cf09bc4..a25cbdb11fafcdb4faf0479fbd623af1b7264e70 100644 (file)
@@ -1,17 +1,36 @@
-nCicCoercion.cmx : nDiscriminationTree.cmx nCicUnifHint.cmx \
-    nCicMetaSubst.cmx nCicCoercion.cmi
-nCicCoercion.cmi : nCicUnifHint.cmi
-nCicMetaSubst.cmx : nCicMetaSubst.cmi
+nCicCoercion.cmx : \
+    nDiscriminationTree.cmx \
+    nCicUnifHint.cmx \
+    nCicMetaSubst.cmx \
+    nCicCoercion.cmi
+nCicCoercion.cmi : \
+    nCicUnifHint.cmi
+nCicMetaSubst.cmx : \
+    nCicMetaSubst.cmi
 nCicMetaSubst.cmi :
-nCicRefineUtil.cmx : nCicMetaSubst.cmx nCicRefineUtil.cmi
+nCicRefineUtil.cmx : \
+    nCicMetaSubst.cmx \
+    nCicRefineUtil.cmi
 nCicRefineUtil.cmi :
-nCicRefiner.cmx : nCicUnification.cmx nCicRefineUtil.cmx nCicMetaSubst.cmx \
-    nCicCoercion.cmx nCicRefiner.cmi
-nCicRefiner.cmi : nCicCoercion.cmi
-nCicUnifHint.cmx : nDiscriminationTree.cmx nCicMetaSubst.cmx \
+nCicRefiner.cmx : \
+    nCicUnification.cmx \
+    nCicRefineUtil.cmx \
+    nCicMetaSubst.cmx \
+    nCicCoercion.cmx \
+    nCicRefiner.cmi
+nCicRefiner.cmi : \
+    nCicCoercion.cmi
+nCicUnifHint.cmx : \
+    nDiscriminationTree.cmx \
+    nCicMetaSubst.cmx \
     nCicUnifHint.cmi
 nCicUnifHint.cmi :
-nCicUnification.cmx : nCicUnifHint.cmx nCicMetaSubst.cmx nCicUnification.cmi
-nCicUnification.cmi : nCicCoercion.cmi
-nDiscriminationTree.cmx : nDiscriminationTree.cmi
+nCicUnification.cmx : \
+    nCicUnifHint.cmx \
+    nCicMetaSubst.cmx \
+    nCicUnification.cmi
+nCicUnification.cmi : \
+    nCicCoercion.cmi
+nDiscriminationTree.cmx : \
+    nDiscriminationTree.cmi
 nDiscriminationTree.cmi :
index cfb9d1b6b8e927ba78f2e0918d22331e98080656..7447a68f2e70dd540be9584157083e4c09ceec74 100644 (file)
@@ -21,7 +21,7 @@ module COT : Set.OrderedType
 with type t = string * NCic.term * int * int  * NCic.term * NCic.term = 
   struct
      type t = string * NCic.term * int * int * NCic.term * NCic.term
-     let compare = Pervasives.compare
+     let compare = Stdlib.compare
   end
 
 module CoercionSet = Set.Make(COT)
index 5c7f92f999a4d10265bdd67a7d7c53375fb85b4c..d37ec4032b6dcff26bbbcd507bcda882fd98b53a 100644 (file)
@@ -21,14 +21,14 @@ with type t = int * NCic.term  * NCic.term * NCic.term =
   struct
         (* precedence, skel1, skel2, term *)
         type t = int * NCic.term * NCic.term * NCic.term
-        let compare = Pervasives.compare
+        let compare = Stdlib.compare
   end
 
 module EOT : Set.OrderedType 
 with type t = int * NCic.term =
   struct
         type t = int * NCic.term 
-        let compare = Pervasives.compare
+        let compare = Stdlib.compare
   end
 
 module HintSet = Set.Make(HOT)
@@ -310,7 +310,7 @@ let look_for_hint (status:#status) metasenv subst context t1 t2 =
     rc
   in
   let rc = 
-    List.sort (fun (x,_,_,_) (y,_,_,_) -> Pervasives.compare x y) rc
+    List.sort (fun (x,_,_,_) (y,_,_,_) -> Stdlib.compare x y) rc
   in 
   let rc = List.map (fun (_,x,y,z) -> x,y,z) rc in
 
index 7d8a45d0e6d9b660ca9f618e7dc25e7b3e858a24..553e1e6716654ebcc9a62de0c6d561b69b2bbdb5 100644 (file)
@@ -19,7 +19,7 @@ exception KeepReducingThis of
   string Lazy.t * (NCicReduction.machine * bool) * 
                   (NCicReduction.machine * bool) ;;
 
-let (===) x y = Pervasives.compare x y = 0 ;;
+let (===) x y = Stdlib.compare x y = 0 ;;
 
 let mk_msg (status:#NCic.status) metasenv subst context t1 t2 =
  (lazy (
index 4d746ad8baf2f74fa3ff83c4936f08d214c45891..b5338715dfd35936fc8f11f8ea9a89e6bb104c44 100644 (file)
@@ -29,7 +29,7 @@ open Discrimination_tree
 
 module TermOT : Set.OrderedType with type t = NCic.term = struct 
   type t = NCic.term 
-  let compare = Pervasives.compare 
+  let compare = Stdlib.compare 
 end
 
 module TermSet = Set.Make(TermOT)
@@ -37,7 +37,7 @@ module TermSet = Set.Make(TermOT)
 module TermListOT : Set.OrderedType with type t = NCic.term list =
  struct
    type t = NCic.term list
-   let compare = Pervasives.compare
+   let compare = Stdlib.compare
  end
 
 module TermListSet : Set.S with type elt = NCic.term list =
@@ -91,8 +91,8 @@ let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
        let x = NReference.compare u1 u2 in
-       if x = 0 then Pervasives.compare a1 a2 else x
-  | e1,e2 -> Pervasives.compare e1 e2
+       if x = 0 then Stdlib.compare a1 a2 else x
+  | e1,e2 -> Stdlib.compare e1 e2
 ;;
 
 let string_of_path l = String.concat "." (List.map ppelem l) ;;
index 75b2d57f87f018d18706b67a4f16e67ea2b71b8c..ca420895d92c48c446b4bd70d62ac525f1353e7a 100644 (file)
@@ -1,22 +1,55 @@
-continuationals.cmx : continuationals.cmi
+continuationals.cmx : \
+    continuationals.cmi
 continuationals.cmi :
-declarative.cmx : nnAuto.cmx nTactics.cmx nTacStatus.cmx nCicElim.cmx \
-    continuationals.cmx declarative.cmi
-declarative.cmi : nnAuto.cmi nTacStatus.cmi
-nCicElim.cmx : nCicElim.cmi
+declarative.cmx : \
+    nnAuto.cmx \
+    nTactics.cmx \
+    nTacStatus.cmx \
+    nCicElim.cmx \
+    continuationals.cmx \
+    declarative.cmi
+declarative.cmi : \
+    nnAuto.cmi \
+    nTacStatus.cmi
+nCicElim.cmx : \
+    nCicElim.cmi
 nCicElim.cmi :
-nCicTacReduction.cmx : nCicTacReduction.cmi
+nCicTacReduction.cmx : \
+    nCicTacReduction.cmi
 nCicTacReduction.cmi :
-nDestructTac.cmx : nTactics.cmx nTacStatus.cmx continuationals.cmx \
+nDestructTac.cmx : \
+    nTactics.cmx \
+    nTacStatus.cmx \
+    continuationals.cmx \
     nDestructTac.cmi
-nDestructTac.cmi : nTacStatus.cmi
-nInversion.cmx : nTactics.cmx nTacStatus.cmx nCicElim.cmx \
-    continuationals.cmx nInversion.cmi
-nInversion.cmi : nTacStatus.cmi
-nTacStatus.cmx : nCicTacReduction.cmx continuationals.cmx nTacStatus.cmi
-nTacStatus.cmi : continuationals.cmi
-nTactics.cmx : nTacStatus.cmx nCicElim.cmx continuationals.cmx nTactics.cmi
-nTactics.cmi : nTacStatus.cmi
-nnAuto.cmx : nTactics.cmx nTacStatus.cmx nCicTacReduction.cmx \
-    continuationals.cmx nnAuto.cmi
-nnAuto.cmi : nTacStatus.cmi
+nDestructTac.cmi : \
+    nTacStatus.cmi
+nInversion.cmx : \
+    nTactics.cmx \
+    nTacStatus.cmx \
+    nCicElim.cmx \
+    continuationals.cmx \
+    nInversion.cmi
+nInversion.cmi : \
+    nTacStatus.cmi
+nTacStatus.cmx : \
+    nCicTacReduction.cmx \
+    continuationals.cmx \
+    nTacStatus.cmi
+nTacStatus.cmi : \
+    continuationals.cmi
+nTactics.cmx : \
+    nTacStatus.cmx \
+    nCicElim.cmx \
+    continuationals.cmx \
+    nTactics.cmi
+nTactics.cmi : \
+    nTacStatus.cmi
+nnAuto.cmx : \
+    nTactics.cmx \
+    nTacStatus.cmx \
+    nCicTacReduction.cmx \
+    continuationals.cmx \
+    nnAuto.cmi
+nnAuto.cmi : \
+    nTacStatus.cmi
index 118261af027c2efa101facb0d21a39d611b03a0e..819160eab02a149e48a637c86ffa599efe015c11 100644 (file)
@@ -568,8 +568,8 @@ let compare e1 e2 =
   match e1,e2 with
   | Constant (u1,a1),Constant (u2,a2) -> 
        let x = NUri.compare u1 u2 in
-       if x = 0 then Pervasives.compare a1 a2 else x
-  | e1,e2 -> Pervasives.compare e1 e2
+       if x = 0 then Stdlib.compare a1 a2 else x
+  | e1,e2 -> Stdlib.compare e1 e2
 ;;
 
 
@@ -578,7 +578,7 @@ end
 module Ncic_termOT : Set.OrderedType with type t = cic_term =
  struct
    type t = cic_term
-   let compare = Pervasives.compare
+   let compare = Stdlib.compare
  end
 
 module Ncic_termSet : Set.S with type elt = cic_term = Set.Make(Ncic_termOT)
index d371409d2ecac8587947476abcba11087074d43d..2dc0be3f443cbc9609eddba7bbe2239ec328d807 100644 (file)
@@ -70,7 +70,7 @@ let print_stat _status tbl =
   let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
   let relevance v = float !(v.uses) /. float !(v.nominations) in
   let vcompare (_,v1) (_,v2) =
-    Pervasives.compare (relevance v1) (relevance v2) in
+    Stdlib.compare (relevance v1) (relevance v2) in
   let l = List.sort vcompare l in
   let short_name r = 
     Filename.chop_extension 
@@ -1490,7 +1490,7 @@ let pp_goals status l =
 module M = 
   struct 
     type t = int
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end
 ;;
 
index f282104465c4bc6d90927ebb77b2a2fe5e48e67f..c8aaec5311e660965c2f1335f3b1bf9a287db096 100644 (file)
@@ -1,2 +1,3 @@
-helm_registry.cmx : helm_registry.cmi
+helm_registry.cmx : \
+    helm_registry.cmi
 helm_registry.cmi :
index f3309633b72d37748793c21bcfbbb6533f8a59d9..c6b2a58fd8afc92c993a419065033b6bb64baea3 100644 (file)
@@ -412,7 +412,7 @@ let ls registry prefix =
         | _ -> assert false)
       ([], []) matching_keys
   in
-  (list_uniq (List.sort Pervasives.compare sections), keys)
+  (list_uniq (List.sort Stdlib.compare sections), keys)
 
 (** {2 API implementation}
  * functional methods above are wrapped so that they work on a default
index 8b3261bc8dffab9f1027b21f36125b37d79a49e2..8863d5405df5eaa6397b4e87407b07ce75d3a21d 100644 (file)
@@ -1,5 +1,11 @@
-utf8Macro.cmo : utf8MacroTable.cmo utf8Macro.cmi
-utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmo : \
+    utf8MacroTable.cmi \
+    utf8Macro.cmi
+utf8Macro.cmx : \
+    utf8MacroTable.cmx \
+    utf8Macro.cmi
 utf8Macro.cmi :
-utf8MacroTable.cmo :
-utf8MacroTable.cmx :
+utf8MacroTable.cmo : \
+    utf8MacroTable.cmi
+utf8MacroTable.cmx : \
+    utf8MacroTable.cmi
index 98ac1d844e00cb9bd07f41a86482f326bdaf4fb4..84b72a664353560f9eb22d9d96a996fe8fbded03 100644 (file)
@@ -1,3 +1,5 @@
-utf8Macro.cmx : utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmx : \
+    utf8MacroTable.cmx \
+    utf8Macro.cmi
 utf8Macro.cmi :
 utf8MacroTable.cmx :
index c2710d4145d423a1f955673688b041568851f6dc..4f34ae8180cf809c2336429791b9db0259174c6d 100644 (file)
@@ -18,7 +18,7 @@ utf8MacroTable.ml:
        ./make_table $@ $@.txt
 utf8MacroTable.cmo: utf8MacroTable.ml
        @echo "  OCAMLC $<"
-       $(H)@$(OCAMLFIND) ocamlc -c $<
+       $(H)@$(OCAMLFIND) ocamlc -rectypes -c $<
 
 pa_unicode_macro.cmo: pa_unicode_macro.ml utf8Macro.cmo
        @echo "  OCAMLC $<"
@@ -29,7 +29,7 @@ pa_unicode_macro.cma: utf8MacroTable.cmo utf8Macro.cmo pa_unicode_macro.cmo
 
 profiling_macros.cmo: profiling_macros.ml
        @echo "  OCAMLC $<"
-       $(H)@$(OCAMLFIND) ocamlc -package camlp5 -pp "camlp5o -loc loc" -c $<
+       $(H)@$(OCAMLFIND) ocamlc -package camlp5 -package str -pp "camlp5o -loc loc" -c $<
 profiling_macros.cma:profiling_macros.cmo
        @echo "  OCAMLC -a $@"
        $(H)@$(OCAMLFIND) ocamlc -a -o $@ $^
index c95282d58a061d1569a199a59a5ce582e46350d4..090807bce818a9c21f7aa1ffd04e6ee26bdc176b 100644 (file)
@@ -50,7 +50,7 @@ let tex_of_unicode s =
        (Hashtbl.find_all Utf8MacroTable.utf82macro s)
     in
     List.sort 
-      (fun x y -> Pervasives.compare (String.length x) (String.length y)) 
+      (fun x y -> Stdlib.compare (String.length x) (String.length y)) 
       alt
   with Not_found -> []
 
diff --git a/matita/components/syntax_extensions/utf8MacroTable.mli b/matita/components/syntax_extensions/utf8MacroTable.mli
new file mode 100644 (file)
index 0000000..b5f5189
--- /dev/null
@@ -0,0 +1,2 @@
+val macro2utf8 : (string,string) Hashtbl.t
+val utf82macro : (string,string) Hashtbl.t
index 8ee8dbbec0891bf4392eaef92a3ed399c547a59a..e022019dbc099603b597c42b73eb1195618d4414 100644 (file)
@@ -1,4 +1,6 @@
-extThread.cmx : extThread.cmi
+extThread.cmx : \
+    extThread.cmi
 extThread.cmi :
-threadSafe.cmx : threadSafe.cmi
+threadSafe.cmx : \
+    threadSafe.cmi
 threadSafe.cmi :
index d59cccd268c1ed6a1f6efad4dd03abd231daef34..f81775ff20aed86ebd48f2a2a04dc7639bddebbf 100644 (file)
@@ -37,7 +37,7 @@ exception Thread_not_found of Thread.t
 module OrderedPid =
   struct
     type t = int
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end
 module PidSet = Set.Make (OrderedPid)
 
index 36a5438084a6137a7f9158f4fc45a2e82c40d60d..31b27a17643bb267e0ab02c7b1bdae148d4c7217 100644 (file)
@@ -1,4 +1,6 @@
-xml.cmx : xml.cmi
+xml.cmx : \
+    xml.cmi
 xml.cmi :
-xmlPushParser.cmx : xmlPushParser.cmi
+xmlPushParser.cmx : \
+    xmlPushParser.cmi
 xmlPushParser.cmi :
index 04b7da8bdaf2fd1da221d42bca31b30539fe4bcb..ba25fab4df555843fd60d3b4cb820bded94c27d6 100644 (file)
@@ -1,4 +1,5 @@
-AC_INIT(matita/matitaTypes.ml)
+AC_INIT
+AC_CONFIG_SRCDIR([matita/matitaTypes.ml])
 
 # Distribution settings
 # (i.e. settings (automatically) manipulated before a release)
@@ -63,6 +64,7 @@ echo "done"
 FINDLIB_LIBSREQUIRES="\
 expat \
 http \
+camlp-streams \
 pcre \
 str \
 unix \
@@ -205,11 +207,12 @@ AC_SUBST(RT_BASE_DIR)
 AC_SUBST(SRCROOT)
 AC_SUBST(TRANSFORMER_MODULE)
 
-AC_OUTPUT([
+AC_CONFIG_FILES([
   components/extlib/componentsConf.ml
   matita/matita.conf.xml
   matita/buildTimeConf.ml
   matita/help/C/version.txt
   Makefile.defs
 ])
+AC_OUTPUT
 
index 447ce30aaed82deb2ede210c8bc1211e4a6fdce7..f1994ce595bd41e306aae2c28d10bfb7a7b36b93 100644 (file)
-applyTransformation.cmx : applyTransformation.cmi
+applyTransformation.cmx : \
+    applyTransformation.cmi
 applyTransformation.cmi :
 buildTimeConf.cmx :
-cicMathView.cmx : matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
-    buildTimeConf.cmx applyTransformation.cmx cicMathView.cmi
-cicMathView.cmi : matitaGuiTypes.cmi applyTransformation.cmi
-lablGraphviz.cmx : lablGraphviz.cmi
+cicMathView.cmx : \
+    matitaMisc.cmx \
+    matitaGuiTypes.cmi \
+    matitaGtkMisc.cmx \
+    buildTimeConf.cmx \
+    applyTransformation.cmx \
+    cicMathView.cmi
+cicMathView.cmi : \
+    matitaGuiTypes.cmi \
+    applyTransformation.cmi
+lablGraphviz.cmx : \
+    lablGraphviz.cmi
 lablGraphviz.cmi :
-matita.cmx : predefined_virtuals.cmx matitaScript.cmx matitaMisc.cmx \
-    matitaInit.cmx matitaGui.cmx buildTimeConf.cmx applyTransformation.cmx
-matitaEngine.cmx : applyTransformation.cmx matitaEngine.cmi
-matitaEngine.cmi : applyTransformation.cmi
-matitaExcPp.cmx : matitaEngine.cmx matitaExcPp.cmi
+matita.cmx : \
+    predefined_virtuals.cmx \
+    matitaScript.cmx \
+    matitaMisc.cmx \
+    matitaInit.cmx \
+    matitaGui.cmx \
+    buildTimeConf.cmx \
+    applyTransformation.cmx
+matitaEngine.cmx : \
+    applyTransformation.cmx \
+    matitaEngine.cmi
+matitaEngine.cmi : \
+    applyTransformation.cmi
+matitaExcPp.cmx : \
+    matitaEngine.cmx \
+    matitaExcPp.cmi
 matitaExcPp.cmi :
 matitaGeneratedGui.cmx :
-matitaGtkMisc.cmx : matitaGeneratedGui.cmx buildTimeConf.cmx \
+matitaGtkMisc.cmx : \
+    matitaGeneratedGui.cmx \
+    buildTimeConf.cmx \
     matitaGtkMisc.cmi
-matitaGtkMisc.cmi : matitaGeneratedGui.cmx
-matitaGui.cmx : matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
-    matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
-    matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
-matitaGui.cmi : matitaGuiTypes.cmi
+matitaGtkMisc.cmi : \
+    matitaGeneratedGui.cmx
+matitaGui.cmx : \
+    matitaTypes.cmx \
+    matitaScript.cmx \
+    matitaMisc.cmx \
+    matitaMathView.cmx \
+    matitaGuiTypes.cmi \
+    matitaGtkMisc.cmx \
+    matitaGeneratedGui.cmx \
+    matitaExcPp.cmx \
+    buildTimeConf.cmx \
+    matitaGui.cmi
+matitaGui.cmi : \
+    matitaGuiTypes.cmi
 matitaGuiInit.cmx :
-matitaGuiTypes.cmi : matitaGeneratedGui.cmx applyTransformation.cmi
-matitaInit.cmx : matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
+matitaGuiTypes.cmi : \
+    matitaGeneratedGui.cmx \
+    applyTransformation.cmi
+matitaInit.cmx : \
+    matitaExcPp.cmx \
+    buildTimeConf.cmx \
+    matitaInit.cmi
 matitaInit.cmi :
-matitaMathView.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
-    matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
-    matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
-    applyTransformation.cmx matitaMathView.cmi
-matitaMathView.cmi : matitaTypes.cmi matitaGuiTypes.cmi
-matitaMisc.cmx : matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
-matitaMisc.cmi : matitaGuiTypes.cmi
-matitaScript.cmx : virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
-    matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \
-    buildTimeConf.cmx matitaScript.cmi
+matitaMathView.cmx : \
+    virtuals.cmx \
+    matitaTypes.cmx \
+    matitaMisc.cmx \
+    matitaGuiTypes.cmi \
+    matitaGtkMisc.cmx \
+    matitaGeneratedGui.cmx \
+    matitaExcPp.cmx \
+    lablGraphviz.cmx \
+    cicMathView.cmx \
+    buildTimeConf.cmx \
+    applyTransformation.cmx \
+    matitaMathView.cmi
+matitaMathView.cmi : \
+    matitaTypes.cmi \
+    matitaGuiTypes.cmi
+matitaMisc.cmx : \
+    matitaGuiTypes.cmi \
+    buildTimeConf.cmx \
+    matitaMisc.cmi
+matitaMisc.cmi : \
+    matitaGuiTypes.cmi
+matitaScript.cmx : \
+    virtuals.cmx \
+    matitaTypes.cmx \
+    matitaMisc.cmx \
+    matitaMathView.cmx \
+    matitaGtkMisc.cmx \
+    matitaEngine.cmx \
+    cicMathView.cmx \
+    buildTimeConf.cmx \
+    matitaScript.cmi
 matitaScript.cmi :
-matitaTypes.cmx : matitaTypes.cmi
+matitaTypes.cmx : \
+    matitaTypes.cmi
 matitaTypes.cmi :
-matitac.cmx : matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaExcPp.cmx \
+matitac.cmx : \
+    matitaclean.cmx \
+    matitaMisc.cmx \
+    matitaInit.cmx \
+    matitaExcPp.cmx \
     matitaEngine.cmx
-matitaclean.cmx : matitaMisc.cmx matitaInit.cmx matitaclean.cmi
+matitaclean.cmx : \
+    matitaMisc.cmx \
+    matitaInit.cmx \
+    matitaclean.cmi
 matitaclean.cmi :
-predefined_virtuals.cmx : virtuals.cmx predefined_virtuals.cmi
+predefined_virtuals.cmx : \
+    virtuals.cmx \
+    predefined_virtuals.cmi
 predefined_virtuals.cmi :
-virtuals.cmx : virtuals.cmi
+virtuals.cmx : \
+    virtuals.cmi
 virtuals.cmi :
index d40a15c7a6eb5d4286d2ecae4d01fd1ce6dd6188..5276991102b4fffba0074c09f08839a9c9f3092d 100644 (file)
@@ -11,7 +11,8 @@ else
   ANNOTOPTION =
 endif
 
-OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7
+#OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-70-31
+OCAML_FLAGS = -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-70-31-29
 OCAMLDEP_FLAGS = -pp $(CAMLP5O) 
 PKGS = -package "$(MATITA_REQUIRES)"
 CPKGS = -package "$(MATITA_CREQUIRES)"
index ec42ee8df543f0fd7db44d8372a96874cbc244e0..8f6bd620423c8dce67bfeec6db229cbf2dbe2d23 100644 (file)
@@ -637,7 +637,7 @@ object (self)
   val mutable current_mathml = None
 
   method nload_sequent:
-   'status. #ApplyTransformation.status as 'status -> NCic.metasenv ->
+   'status. (#ApplyTransformation.status as 'status) -> NCic.metasenv ->
      NCic.substitution -> int -> unit
    = fun status metasenv subst metano ->
     let sequent = List.assoc metano metasenv in
@@ -654,7 +654,7 @@ object (self)
     self#load_root ~root:txt
 
   method load_nobject :
-   'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit
+   'status. (#ApplyTransformation.status as 'status) -> NCic.obj -> unit
    = fun status obj ->
     let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false
     80 status obj in
@@ -675,7 +675,7 @@ object (self)
           ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
         end;*)
         self#load_root ~root:txt;
-        (*current_mathml <- Some mathml*)(*)*);
+        (*current_mathml <- Some mathml*)(* ) *);
 end
 
  (** constructors *)
@@ -686,7 +686,7 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi
       GContainer.pack_container ~create:(fun pl ->
         let obj = SourceView.new_ () in
         Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl;
-        new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView)
+        new _cicMathView obj)(* )) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView)
 
 let screenshot _status _sequents _metasenv _subst (_filename (*as ofn*)) =
  () (*MATITA 1.0
index e31efac1f9a3134168f6c9fe34c279c812b38844..2d6e3b431046ca6be164f7411e3fb1b5326eb5e4 100644 (file)
@@ -41,7 +41,7 @@ let read_dir file =
     Filename.remove_extension name
   in
   let dir = Array.to_list (Sys.readdir file) in
-  let mods = List.fast_sort Pervasives.compare (list_rev_filter_map filter map dir) in
+  let mods = List.fast_sort Stdlib.compare (list_rev_filter_map filter map dir) in
   {
     ET.cdir = file; mods;
   }
@@ -62,7 +62,7 @@ let read_index dir =
     try read_mods mods ich with
     | End_of_file -> close_in ich 
   end;
-  let mods = List.fast_sort Pervasives.compare !mods in
+  let mods = List.fast_sort Stdlib.compare !mods in
   {
     ET.cdir = dir; mods;
   }
index b0a5c7f12cbf91acb1e251c76d039cf564cf9309..169800e5997fd6ee92e46e7f64bc77906090140c 100644 (file)
@@ -106,7 +106,7 @@ let compact_disambiguation_errors all_passes errorll =
       filter choices
    in
     filter_phase_3
-     (List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
+     (List.map (fun (o,l) -> o,List.sort choices_compare_by_passes l)
        (uniq (List.stable_sort choices_compare choices)))
   in
    choices
@@ -155,8 +155,7 @@ let rec to_string exn =
   | MatitaEngine.TryingToAdd msg ->
      None, "Attempt to insert an alias in batch mode: " ^ Lazy.force msg
   | MatitaEngine.AlreadyLoaded msg ->
-     None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is
-     already loaded; undo the inclusion and try again."
+     None, "The file " ^ Lazy.force msg ^ " needs recompilation but it is already loaded; undo the inclusion and try again."
   | MatitaEngine.FailureCompiling (filename,exn) ->
      None, "Compiling " ^ filename ^ ":\n" ^ snd (to_string exn)
   | NCicRefiner.AssertFailure msg ->
index 04a531216780997863f7bad05f0d26dc3dab826c..6884e232e1c686f8194c038eb73b59973f079a2f 100644 (file)
@@ -76,7 +76,9 @@ class multiStringListModel:
     method list_store: GTree.list_store (** list_store forwarding *)
 
     method easy_mappend:     string list -> unit        (** append + set *)
+
     method easy_minsert:     int -> string list -> unit (** insert + set *)
+
     method easy_mselection:  unit -> string list list
   end
   
@@ -87,7 +89,9 @@ class stringListModel:
     inherit multiStringListModel
 
     method easy_append:     string -> unit        (** append + set *)
+
     method easy_insert:     int -> string -> unit (** insert + set *)
+
     method easy_selection:  unit -> string list
   end
   
index ad34b7a5773c85aa87ee5bebe025f6e977ce0707..7e2b0401bbc41659bc60e8a9f0e1c4735efa6450 100644 (file)
@@ -169,7 +169,7 @@ class interpErrorModel =
         tree_store#clear ();
         let idx1 = ref ~-1 in
         List.iter
-          (fun _,lll ->
+          (fun (_,lll) ->
             incr idx1;
             let loc_row =
              if List.length choices = 1 then
@@ -196,7 +196,7 @@ class interpErrorModel =
                 Some loc_row) in
             let idx2 = ref ~-1 in
              List.iter
-              (fun passes,envs_and_diffs,_,_ ->
+              (fun (passes,envs_and_diffs,_,_) ->
                 incr idx2;
                 let msg_row =
                  if List.length lll = 1 then
@@ -375,7 +375,7 @@ let interactive_error_interp ~all_passes
          String.concat "\n"
           ("" ::
             List.map
-             (fun k,desc -> 
+             (fun (k,desc) -> 
                let alias =
                 match k with
                 | DisambiguateTypes.Id id ->
@@ -716,7 +716,6 @@ class gui () =
           "apply rule (∃#e (…) {…} […] (…));\n\t[\n\t|\n\t]\n");
 
     
-      let module Hr = Helm_registry in
       MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem
         ~callback:(function 
           | true -> main#toplevel#fullscreen () 
index 2c2a818a27fa125be81cd7ccbc21730c55823150..9f7ae3ac2306183c2bdd03d538d2c25c74af9c5d 100644 (file)
@@ -59,7 +59,7 @@ let registry_defaults = [
 
 let set_registry_values =
   List.iter 
-    (fun key, value -> 
+    (fun (key, value) -> 
        if not (Helm_registry.has key) then Helm_registry.set ~key ~value)
 
 let fill_registry init_status =
@@ -116,7 +116,7 @@ let initialize_environment init_status =
   
 let status = ref []
 
-let usages = Hashtbl.create 11 (** app name (e.g. "matitac") -> usage string *)
+let usages = Hashtbl.create 11 (* app name (e.g. "matitac") -> usage string *)
 let _ =
   List.iter
     (fun (name, s) -> Hashtbl.replace usages name s)
index 271a7b19ab45c664f61aac4c805b435d81415044..93a0b65eaa392b970abcf1d26108ffeb2b27c58f 100644 (file)
@@ -97,7 +97,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       goal2win <- [];
       _metasenv <- [],[]
 
-    method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
+    method nload_sequents : 'status. (#GrafiteTypes.status as 'status) -> unit
     = fun (status : #GrafiteTypes.status) ->
      let _,_,metasenv,subst,_ = status#obj in
       _metasenv <- metasenv,subst;
@@ -151,7 +151,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         end
       in
       let add_switch _ _ (_, sw) = add_tab (render_switch sw) sw in
-      Stack.iter  (** populate notebook with tabs *)
+      Stack.iter  (* populate notebook with tabs *)
         ~env:(fun depth _tag (pos, sw) ->
           let markup =
             match depth, pos with
@@ -172,7 +172,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           self#render_page status ~page ~goal_switch))
 
     method private render_page:
-     'status. #ApplyTransformation.status as 'status -> page:int ->
+     'status. (#ApplyTransformation.status as 'status) -> page:int ->
        goal_switch:Stack.switch -> unit
      = fun status ~page:_ ~goal_switch ->
       (match goal_switch with
@@ -204,7 +204,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
              (w#vadjustment#upper -. w#vadjustment#page_size));
       with Not_found -> assert false)
 
-    method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
+    method goto_sequent: 'status. (#ApplyTransformation.status as 'status) -> int -> unit
      = fun status goal ->
       let goal_switch, page =
         try
@@ -532,10 +532,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           (Virtuals.get_all_eqclass ()));
       Printf.bprintf b "\n\nVirtual keys (trigger with ALT-L):\n\n";
       List.iter 
-        (fun tag, items -> 
+        (fun (tag, items) -> 
            Printf.bprintf b "  %s:\n" tag;
            List.iter 
-             (fun names, symbol ->
+             (fun (names, symbol) ->
                 Printf.bprintf b "  \t%s\t%s\n" 
                   (Glib.Utf8.from_unichar symbol)
                   (String.concat ", " names))
index dd1e189557ba88cb7bdba3a0b063d9d091631823..567f67d42059798224ec7b63673e4f604b04b6fe 100644 (file)
@@ -30,6 +30,7 @@ val sequentsViewer_instance: GPack.notebook -> MatitaGuiTypes.sequentsViewer
 val refresh_all_browsers: unit -> unit  (** act on all cicBrowsers *)
 
 (** {2 Rendering in a browser} *)
+
 (** @param reuse if set reused last opened cic browser otherwise 
 *  opens a new one. default is false *)
 val cicBrowser: ?reuse:bool -> MatitaTypes.mathViewer_entry option -> unit
@@ -42,6 +43,7 @@ val has_selection: unit -> bool
    * @raise Failure "no selection" *)
 val copy_selection: unit -> unit
 val has_clipboard: unit -> bool (** clipboard is not empty *)
+
 val empty_clipboard: unit -> unit (** empty the clipboard *)
 
   (** @raise Failure "empty clipboard" *)
index 53d1d1f67ec2440c2c3ce45df0958ab52b9edfd3..e773fc977c6efb27a6328ab6c5d368377b72ff63 100644 (file)
@@ -38,8 +38,8 @@ let strip_suffix ~suffix s =
 let absolute_path file =
   if file.[0] = '/' then file else Unix.getcwd () ^ "/" ^ file
   
-let is_proof_script _fname = true  (** TODO Zack *)
-let is_proof_object _fname = true  (** TODO Zack *)
+let is_proof_script _fname = true  (* TODO Zack *)
+let is_proof_object _fname = true  (* TODO Zack *)
 
 let append_phrase_sep s =
   if not (Pcre.pmatch ~pat:(sprintf "%s$" BuildTimeConf.phrase_sep) s) then
index b3bd617b2d69c04ec13e5cf3c72a8f144856ca7c..c189861c65a65cad7373c70e5926e33329c2ec62 100644 (file)
@@ -35,7 +35,8 @@ val is_proof_object: string -> bool
   * it *)
 val append_phrase_sep: string -> string
 
-val normalize_dir: string -> string (** add trailing "/" if missing *)
+  (** add trailing "/" if missing *)
+val normalize_dir: string -> string
 val strip_suffix: suffix:string -> string -> string
 
   (** @return tl tail of a list starting at a given element
@@ -50,8 +51,12 @@ type 'a memento
 class type ['a] history =
   object ('b)
     method add : 'a -> unit
-    method next : 'a        (** @raise History_failure *)
-    method previous : 'a    (** @raise History_failure *)
+
+     (** @raise History_failure *)
+    method next : 'a
+
+     (** @raise History_failure *)
+    method previous : 'a
     method load: 'a memento -> unit
     method save: 'a memento
     method is_begin: bool 
index c39e1de40a5ec9d9d7856718f196787ba9a4c1b3..2401221344c43de37f287d89afbd0f8156128065 100644 (file)
@@ -102,7 +102,7 @@ let eval_nmacro _include_paths (_buffer : GText.buffer) status _unparsed_text pa
        let name = Filename.dirname (script#filename) ^ "/" ^ name in
        let sequents = 
          let selected = Continuationals.Stack.head_goals status#stack in
-         List.filter (fun x,_ -> List.mem x selected) menv         
+         List.filter (fun (x,_) -> List.mem x selected) menv         
        in
        CicMathView.screenshot status sequents menv subst name;
        [status, parsed_text], "", parsed_text_length
index f90ab14bdbe39c9352c1167faa4b7ea1c5a47326..45f3829dd789b67f361b59bea3d925281d1a85f0 100644 (file)
@@ -1497,7 +1497,7 @@ let predefined_virtuals = [
 
 let load_predefined_virtuals () =
   List.iter 
-    (fun a,b,c -> 
+    (fun (a,b,c) -> 
        Virtuals.add_virtual a (Glib.Utf8.first_char b) c) 
     predefined_virtuals
 ;;