From eb56a0fcc6f9f91064b6b0707e92c3b734457ccd Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 13 Mar 2019 13:58:48 +0100 Subject: Fix for CompCert 3.5 --- mppa_k1c/abstractbb/Impure/ImpPrelude.v | 1 + 1 file changed, 1 insertion(+) (limited to 'mppa_k1c/abstractbb') diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index 46f2d387..e7c7a9fb 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -4,6 +4,7 @@ Require Extraction. Require Import Ascii. Require Import BinNums. Require Export ImpCore. +Require Export PArith. Axiom caml_string: Type. Extract Constant caml_string => "string". -- cgit