Merge pull request rocq-community#71 from coq-community/theories

proux01 · web-flow · commit d0df5b05d689 · 2021-08-24T10:49:46.000+02:00
introduce Params.v file
diff --git a/.gitignore b/.gitignore
@@ -1,6 +1,9 @@
 # Generated Makefile
-/Makefile.coq
-/Makefile.coq.conf
+Makefile.coq
+Makefile.coq.conf
+
+# Dune
+_build
 
 # Make dependencies
 *.d
diff --git a/Makefile b/Makefile
@@ -1,14 +1,16 @@
-# -*- Makefile -*-
-.PHONY: coq clean
+all: Makefile.coq
+	@+$(MAKE) -f Makefile.coq all
 
-coq:: Makefile.coq
-	$(MAKE) -f Makefile.coq
+clean: Makefile.coq
+	@+$(MAKE) -f Makefile.coq cleanall
+	@rm -f Makefile.coq Makefile.coq.conf
 
-Makefile.coq: Make.cfg
-	coq_makefile -f Make.cfg -o Makefile.coq
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
 
-distclean:
-	rm -f Makefile.coq Makefile.coq.conf Makefile.coq.bak .coqdeps.d
+force _CoqProject Makefile: ;
 
-install:
-	$(MAKE) -f Makefile.coq install
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
+.PHONY: all clean force
diff --git a/_CoqProject b/_CoqProject
@@ -1,3 +1,4 @@
+-R theories Param
 -R src Param
 -I src
 src/debug.ml
@@ -6,3 +7,4 @@ src/relations.ml
 src/declare_translation.ml
 src/abstraction.mlg
 src/paramcoq.mlpack
+theories/Param.v
diff --git a/dune-project b/dune-project
@@ -0,0 +1,3 @@
+(lang dune 2.5)
+(using coq 0.2)
+(name paramcoq)
diff --git a/src/dune b/src/dune
@@ -1,11 +1,8 @@
 (library
  (name paramcoq)
- (public_name coq.plugins.paramcoq)
- (synopsis "Coq Plugin for Parametricity")
- (flags :standard -warn-error -3)
- (libraries coq.plugins.ltac))
+ (public_name coq-paramcoq.plugin)
+ (synopsis "Plugin for generating parametricity statements to perform refinement proofs")
+ (flags :standard -rectypes -w -9-27)
+ (libraries coq-core.plugins.ltac))
 
-(rule
- (targets abstraction.ml)
- (deps (:pp-file abstraction.mlg) )
- (action (run coqpp %{pp-file})))
+(coq.pp (modules abstraction))
diff --git a/theories/Param.v b/theories/Param.v
@@ -0,0 +1 @@
+Declare ML Module "paramcoq".
diff --git a/theories/dune b/theories/dune
@@ -0,0 +1,5 @@
+(coq.theory
+ (name Param)
+ (package coq-paramcoq)
+ (synopsis "Plugin for generating parametricity statements to perform refinement proofs")
+ (libraries coq-paramcoq.plugin))

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+(lang dune 2.5)`
	`2`	`+(using coq 0.2)`
	`3`	`+(name paramcoq)`