Le 30/01/2018 à 16:47, Guillaume Melquiond a écrit : >> Would it be possible to adapt this file in such a >> way that it uses >> Big_int_Z instead of Big_int if Zarith is available (as it is done in >> lib/ocaml/why3__BigInt.ml)? > > I don't think so. If I remember correctly, the main issue is that using > Zarith in that file breaks the Why3 plugin for Coq. I am unfortunately > not savvy enough with the intricacies of dynamic linking in OCaml to > understand what is needed to make it work.
Indeed, but since we are considering giving up the support of that Coq plugin, the issue may disappear in the near future. Or, as well, if Coq also gives up its usage of Num and uses Zarith instead. But it is not the only issue: we also have the TryWhy3 interface which uses js_of_ocaml, and if there is a binding of Num in js_of_ocaml, I don't know if there is one for Zarith. - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Île-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
