From de61c7d77e49286622c4aebd56f2e87b0df93903 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sat, 5 Apr 2014 19:51:04 -0400 Subject: Had to split Nativelambda in two files because of Retroknowledge dependencies. --- kernel/nativeinstr.mli | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 kernel/nativeinstr.mli (limited to 'kernel/nativeinstr.mli') diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli new file mode 100644 index 000000000..4e0291ed9 --- /dev/null +++ b/kernel/nativeinstr.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(*