1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(*
* The Why certification tool
* Copyright (C) 2002 Jean-Christophe FILLIATRE
*
* This software is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public
* License version 2, as published by the Free Software Foundation.
*
* This software is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
*
* See the GNU General Public License version 2 for more details
* (enclosed in the file GPL).
*)
(* Why compatibility file with Coq development version *)
Require Export Bool_nat.
Require Export Zwf.
Require Import LegacyRing.
Tactic Notation "ring" constr(t) := legacy ring.
|
