grobner.ml.patch

183c183,184
<           c1 =/ c2 && (m1 < m2 || m1 = m2 && poly_lt o1 o2) in
---
>           c1 =/ c2 && (List.compare Int.compare m1 m2 = Less ||
>                        m1 = m2 && poly_lt o1 o2) in
217,219c218,220
<     Format.print_string(string_of_int(length basis)^" basis elements and "^
<                         string_of_int(length pairs)^" critical pairs");
<     Format.print_newline();
---
>     print(string_of_int(length basis)^" basis elements and "^
>           string_of_int(length pairs)^" critical pairs");
>     print "\n";
277,278c278
<       Start(-1) -> []
<     | Start m -> [m,[num_1,map (K 0) vars]]
---
>       Start m -> if m = -1 then [] else [m,[num_1,map (K 0) vars]]
285c285
<           let dom = setify(union (map fst lis1) (map fst lis2)) in
---
>           let dom = setify (<) (union (map fst lis1) (map fst lis2)) in
448c448
<       let vars = sort (fun x y -> x < y) (setify rawvars) in
---
>       let vars = sort Term.(<) (setify Term.(<) rawvars) in
483c483,486
<       let rec assoceq a l =
---
>       (* OA Lack of pointer equality makes this useless in Candle,
>             and lack of let polymorphism gets type checking to fail
>             on this definition. *)
>       (* let rec assoceq a l =
486c489
<         | (x,y)::t -> if x==a then y else assoceq a t in
---
>         | (x,y)::t -> if x==a then y else assoceq a t in *)
489,490c492,493
<          (Format.print_string("Generating HOL version of proof");
<           Format.print_newline();
---
>          (print "Generating HOL version of proof";
>           print "\n";
494c497
<             try assoceq prf (!execache) with Failure _ ->
---
>             (* try assoceq prf (!execache) with Failure _ -> *)
505,506c508,509
<          (Format.print_string("Generating HOL version of scaled proof");
<           Format.print_newline();
---
>          (print "Generating HOL version of scaled proof";
>           print "\n";
511c514
<             try assoceq prf (!execache) with Failure _ ->
---
>             (* try assoceq prf (!execache) with Failure _ -> *)
559,560c562,563
<       Format.print_string("Translating certificate to HOL inferences");
<       Format.print_newline();
---
>       print "Translating certificate to HOL inferences";
>       print "\n";
604c607
<     let vars = sort (fun x y -> x < y) (setify rawvars) in
---
>     let vars = sort Term.(<) (setify Term.(<) rawvars) in