diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-02-15 09:55:01 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-02-15 09:55:01 +0100 |
| commit | 29653baeb2c7fa6bfe5da031622d8fb8ac1e50c3 (patch) | |
| tree | 0c6bd91373882c97ddd80f72f53bf8406459d999 /backend/CMtypecheck.mli | |
| parent | d28d699bc848795ff9801faef621ac209e992fa0 (diff) | |
| parent | d000fe3f6df676596b5371f9760cdf0b2922ea11 (diff) | |
| download | compcert-29653baeb2c7fa6bfe5da031622d8fb8ac1e50c3.tar.gz compcert-29653baeb2c7fa6bfe5da031622d8fb8ac1e50c3.zip | |
Merge pull request #170 from AbsInt/remove_cminor
Remove CompCert's ability to parse and compile source files written in Cminor
This facility is no longer used (as far as we know) and is painful to maintain.
Diffstat (limited to 'backend/CMtypecheck.mli')
| -rw-r--r-- | backend/CMtypecheck.mli | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/backend/CMtypecheck.mli b/backend/CMtypecheck.mli deleted file mode 100644 index 44c76544..00000000 --- a/backend/CMtypecheck.mli +++ /dev/null @@ -1,19 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -exception Error of string - -val type_program: Cminor.program -> Cminor.program - |