diff options
| author | Maxime Dénès <mail@maximedenes.fr> | 2020-02-25 08:29:03 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-25 08:29:03 +0100 |
| commit | 82fd19bc1c16782649c741548edb0649522ff900 (patch) | |
| tree | 4ee9b079d4e87cadcef57aecb7c0d03f034b8ade /src/lia/lia.ml | |
| parent | e9cf693337de2a23f433ce382c14ddc528ebc5f6 (diff) | |
| download | smtcoq-82fd19bc1c16782649c741548edb0649522ff900.tar.gz smtcoq-82fd19bc1c16782649c741548edb0649522ff900.zip | |
Do not call Coqlib resolution at linking time (#59)
This was triggering an exception in async mode (and probably with static
linking too), where ML code is loaded before `.vo` files.
Fixes #58
Diffstat (limited to 'src/lia/lia.ml')
| -rw-r--r-- | src/lia/lia.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/lia/lia.ml b/src/lia/lia.ml index d546559..53ee55d 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -117,7 +117,7 @@ let smt_Atom_to_micromega_formula tbl ha = (* specialized fold *) -let default_constr = Structures.econstr_of_constr (mkInt 0) +let default_constr = lazy (Structures.econstr_of_constr (mkInt 0)) let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0 (* morphism for general formulas *) @@ -137,7 +137,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l = match Form.pform l with | Fatom ha -> A (smt_Atom_to_micromega_formula tbl ha, - default_tag,default_constr) + default_tag, Lazy.force default_constr) | Fapp (Ftrue, _) -> TT | Fapp (Ffalse, _) -> FF | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> C (x,y)) TT l |