diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-10 18:41:46 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2015-02-10 18:41:46 +0100 |
| commit | ff9b5494cb1943339543eeac41683a8ec2dda437 (patch) | |
| tree | 21af4c0fff64fbd03c6c2006da1e305e849ebbff /src/lia | |
| parent | 5311b1fa064949089b8d17e34eb31a62426f71fd (diff) | |
| download | smtcoq-ff9b5494cb1943339543eeac41683a8ec2dda437.tar.gz smtcoq-ff9b5494cb1943339543eeac41683a8ec2dda437.zip | |
More on the support for standard Coq (not working yet)
Diffstat (limited to 'src/lia')
| -rw-r--r-- | src/lia/Lia.v | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/src/lia/Lia.v b/src/lia/Lia.v index 0969db0..282523a 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -21,7 +21,6 @@ Require Import RingMicromega. Require Import ZMicromega. Require Import Tauto. Require Import Psatz. -(* Add LoadPath ".." as SMTCoq. *) Require Import Misc State. Require Import SMT_terms. @@ -40,7 +39,7 @@ Section certif. Import EnvRing Atom. - Register option_map as PrimInline. + (* Register option_map as PrimInline. *) Section BuildPositive. Variable build_positive : hatom -> option positive. @@ -62,7 +61,7 @@ Section certif. (PArray.length t_atom) 0 (fun _ => None). Definition build_positive_atom := build_positive_atom_aux build_positive. - Register build_positive_atom as PrimInline. + (* Register build_positive_atom as PrimInline. *) Section BuildZ. @@ -321,7 +320,7 @@ Section certif. | _ => C._true end else C._true. - Register get_eq as PrimInline. + (* Register get_eq as PrimInline. *) Definition get_not_le (l:_lit) (f : Atom.hatom -> Atom.hatom -> C.t) := if negb (Lit.is_pos l) then @@ -334,7 +333,7 @@ Section certif. | _ => C._true end else C._true. - Register get_not_le as PrimInline. + (* Register get_not_le as PrimInline. *) Definition check_micromega cl c : C.t := match build_clause empty_vmap cl with |