From 4c8bae70924de6b904f150a0c4696554fbf9d5db Mon Sep 17 00:00:00 2001 From: acondolu Date: Sun, 10 Jun 2018 17:28:28 +0200 Subject: [PATCH] Using C instead of @ to combine more convergents in p.conv --- ocaml/simple.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 34f9f72..34b2a7f 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -395,8 +395,7 @@ let problem_of (label, div, convs, ps, var_names) = | `N _ | `Match _ -> assert false in assert (List.length ps = 0); let convs = List.rev convs in - let conv = List.fold_left (fun x y -> fst (mk_app x (aux 0 (y :> Num.nf)))) (V (List.length var_names)) convs in - let var_names = "@" :: var_names in + let conv = List.fold_left (fun x y -> fst (mk_app x (aux 0 (y :> Num.nf)))) C convs in let div = match div with | Some div -> aux 0 (div :> Num.nf) | None -> assert false in -- 2.39.2