summaryrefslogtreecommitdiff
path: root/plugins/romega/ROmega.v
blob: 3ddb6bed1294a7521a6141aea1ff93013672a8e6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
(*************************************************************************

   PROJET RNRT Calife - 2001
   Author: Pierre Crégut - France Télécom R&D
   Licence : LGPL version 2.1

 *************************************************************************)

Require Import ReflOmegaCore.
Require Export Setoid.
Require Export PreOmega.
Require Export ZArith_base.
Require Import OmegaPlugin.
Declare ML Module "romega_plugin".