aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 19:52:33 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:33:39 +0200
commita5f33b5fda592c2dfaed0c16d3773b35e7acab28 (patch)
tree6f9acc82475871ee7dd51b434beb791ab3086446 /plugins/micromega
parentf67f84fc4831923aa9a2323b3a71c3a69fe61480 (diff)
Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum
Diffstat (limited to 'plugins/micromega')
-rw-r--r--plugins/micromega/mfourier.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index f4f9b3c2f..377994415 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -99,7 +99,7 @@ module PSet = ISet
module System = Hashtbl.Make(Vect)
type proof =
-| Hyp of int
+| Assum of int
| Elim of var * proof * proof
| And of proof * proof
@@ -134,7 +134,7 @@ exception SystemContradiction of proof
let hyps prf =
let rec hyps prf acc =
match prf with
- | Hyp i -> ISet.add i acc
+ | Assum i -> ISet.add i acc
| Elim(_,prf1,prf2)
| And(prf1,prf2) -> hyps prf1 (hyps prf2 acc) in
hyps prf ISet.empty
@@ -143,7 +143,7 @@ let hyps prf =
(** Pretty printing *)
let rec pp_proof o prf =
match prf with
- | Hyp i -> Printf.fprintf o "H%i" i
+ | Assum i -> Printf.fprintf o "H%i" i
| Elim(v, prf1,prf2) -> Printf.fprintf o "E(%i,%a,%a)" v pp_proof prf1 pp_proof prf2
| And(prf1,prf2) -> Printf.fprintf o "A(%a,%a)" pp_proof prf1 pp_proof prf2
@@ -270,7 +270,7 @@ let norm_cstr {coeffs = v ; op = o ; cst = c} idx =
(match o with
| Eq -> Some c , Some c
| Ge -> Some c , None) ;
- prf = Hyp idx }
+ prf = Assum idx }
(** [load_system l] takes a list of constraints of type [cstr_compat]
@@ -285,7 +285,7 @@ let load_system l =
let vars = List.fold_left (fun vrs (cstr,i) ->
match norm_cstr cstr i with
- | Contradiction -> raise (SystemContradiction (Hyp i))
+ | Contradiction -> raise (SystemContradiction (Assum i))
| Redundant -> vrs
| Cstr(vect,info) ->
xadd_cstr vect info sys ;
@@ -867,7 +867,7 @@ let mk_proof hyps prf =
let rec mk_proof prf =
match prf with
- | Hyp i -> [ ([i, Int 1] , List.nth hyps i) ]
+ | Assum i -> [ ([i, Int 1] , List.nth hyps i) ]
| Elim(v,prf1,prf2) ->
let prfsl = mk_proof prf1