diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-20 10:38:47 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-20 10:38:47 +0100 |
| commit | 07c5e013cbe9aac299881bdde3e1d44af0d35fa8 (patch) | |
| tree | 3d28c4bed80fc7d8ecc25b9d32d112f9b5cbce81 /plugins | |
| parent | 9d3a07d9a7ddf3a0e33b6b1f60d3c89037dc55b7 (diff) | |
| parent | 6af31414f91065a3a97af32b9151a6010792753a (diff) | |
Merge PR #6161: Fix micromega.ml to match generated file and enforce match in make.
Diffstat (limited to 'plugins')
| -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 |