diff options
author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-13 17:11:29 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-01-13 17:11:29 +0100 |
commit | 7072c4591668d2c21211a744d3719f6b42d1e7b9 (patch) | |
tree | 800520e1e414e10b29804a998c63764c18f2c1cd /src/zchaff/zchaff.ml | |
parent | 469a88043ad000403cff5122e27770c130ef77e4 (diff) | |
download | smtcoq-7072c4591668d2c21211a744d3719f6b42d1e7b9.tar.gz smtcoq-7072c4591668d2c21211a744d3719f6b42d1e7b9.zip |
Identify ML functions that depend on native-coq
Diffstat (limited to 'src/zchaff/zchaff.ml')
-rw-r--r-- | src/zchaff/zchaff.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml index b94a0cc..8c07fc7 100644 --- a/src/zchaff/zchaff.ml +++ b/src/zchaff/zchaff.ml @@ -139,7 +139,7 @@ let import_cnf_trace reloc filename first last = let make_roots first last = let cint = Lazy.force cint in - let roots = Array.make (last.id + 2) (Term.mkArray (cint, Array.make 1 (mkInt 0))) in + let roots = Array.make (last.id + 2) (Structures.mkArray (cint, Array.make 1 (mkInt 0))) in let mk_elem l = let x = match Form.pform l with | Fatom x -> x + 2 @@ -150,15 +150,15 @@ let make_roots first last = let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- Term.mkArray (cint, croot); + roots.(!r.id) <- Structures.mkArray (cint, croot); r := next !r done; let root = Array.of_list (get_val !r) in let croot = Array.make (Array.length root + 1) (mkInt 0) in Array.iteri (fun i l -> croot.(i) <- mk_elem l) root; - roots.(!r.id) <- Term.mkArray (cint, croot); + roots.(!r.id) <- Structures.mkArray (cint, croot); - Term.mkArray (mklApp carray [|cint|], roots) + Structures.mkArray (mklApp carray [|cint|], roots) let interp_roots first last = let tbl = Hashtbl.create 17 in |