diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-15 14:20:00 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-16 14:23:07 +0100 |
| commit | 6af31414f91065a3a97af32b9151a6010792753a (patch) | |
| tree | 29242ed58354aa4290e050df073c926b754a498d /plugins/micromega | |
| parent | a2b02cb9142984b912bf01cea09449d767326f19 (diff) | |
Fix micromega.ml to match generated file and enforce match in make.
Mismatch probably caused by c5aca4005.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/micromega.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 7da4a3b82..52c6ef983 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' = (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **) -let and_cnf f1 f2 = - app f1 f2 +let and_cnf = + app (** val xcnf : ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1 @@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **) -let norm cO cI cplus ctimes cminus copp ceqb = - norm_aux cO cI cplus ctimes cminus copp ceqb +let norm = + norm_aux (** val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let psub0 cO cplus cminus copp ceqb = - psub cO cplus cminus copp ceqb +let psub0 = + psub (** val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **) -let padd0 cO cplus ceqb = - padd cO cplus ceqb +let padd0 = + padd (** val xnormalise : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 |