Commit e6432f53 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Rename coq_naturals into CoqNaturals so that the file generated by

coqine has the same basename
parent 82916e9e
......@@ -2,25 +2,23 @@ include ../../.config_vars
include ../../Makefile.rules
FCL_FILES=$(wildcard *.fcl)
all: $(FCL_FILES:.fcl=.dko)
V_FILES=$(wildcard *.v)
all: $(FCL_FILES:.fcl=.dko) $(V_FILES:.v=.dko)
INCLUDE_DIRS= -I ../../core/logic -I ../../core/arith -I ../logic
COQMODULES = holtypes Logic Datatypes Wf
VOS = $(V_FILES:.v=.vo) coq_naturals.vo %.vo
( echo "Require Coqine.";\
echo "Require coq_naturals.";\
echo "Require $*.";\
echo "Dedukti Export All.") | $(COQTOP)
depend: .depend
$(FOCALIZEDEP) $(FCL_FILES) > $@ coq__naturals.dko CoqNaturals.dko
-include .depend
clean :
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend
rm -f *.dko *.sk* *.fo *.pfc *.zv *.mangled *_fcl.* .depend *.vo *.glob *.dk
......@@ -212,7 +212,7 @@ species CoqLe =
inherit NatLeMinusZenon, CoqMinus;
logical let le(m : coq_nat, n : coq_nat) = internal bool
external | dedukti -> {* cbool_to_bool(coq__naturals.leb m n) *};
external | dedukti -> {* cbool_to_bool(CoqNaturals.leb m n) *};
proof of le_zero_n = dedukti proof definition of le, zero
{* (n : cc.eT abst_T => cbool_true). *};
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment