diff options
Diffstat (limited to 'theories/micromega/ZMicromega.v')
| -rw-r--r-- | theories/micromega/ZMicromega.v | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index efb263faf3..bff9671fee 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -564,10 +564,14 @@ Inductive ZArithProof := . (*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*) +Register ZArithProof as micromega.ZArithProof.type. +Register DoneProof as micromega.ZArithProof.DoneProof. +Register RatProof as micromega.ZArithProof.RatProof. +Register CutProof as micromega.ZArithProof.CutProof. +Register EnumProof as micromega.ZArithProof.EnumProof. +Register ExProof as micromega.ZArithProof.ExProof. -(* n/d <= x -> d*x - n >= 0 *) - (* In order to compute the 'cut', we need to express a polynomial P as a * Q + b. - b is the constant |