Port to 8.7.

Nothing remarkable, however the changes in universe polymorphism
should be reviewed.

Author: ejgallego

.gitignore

@@ -0,0 +1,37 @@
+# Generated Makefile
+/Makefile.coq
+/Makefile.coq.conf
+
+# Make dependencies
+*.d
+
+# Backup files
+*.bak
+
+# emacs backup files
+*~
+
+# vim backup files
+\#*\#
+
+# Coq annotation files
+*.glob
+
+# Coq auxiliary files
+.*.aux
+
+# Coq compilation unit
+*.vo
+
+*.annot
+*.cmo
+*.cma
+*.cmi
+*.a
+*.o
+*.cmi
+*.cmt
+*.cmti
+*.cmx
+*.cmxs
+*.cmxa

.merlin

@@ -0,0 +1,6 @@
+FLG -rectypes -thread -w @1..50@59-4-44 -safe-string
+
+S src
+B src
+
+PKG threads threads.posix coq.intf coq.ltac coq.idetop

Make.cfg

@@ -6,4 +6,4 @@ src/parametricity.ml
 src/relations.ml
 src/declare_translation.ml
 src/abstraction.ml4
-src/paramcoq.mllib
+src/paramcoq.mlpack

Makefile

@@ -3,7 +3,7 @@
 coq:: Makefile.coq
 	$(MAKE) -f Makefile.coq
 
-src/paramcoq_mod.ml: src/paramcoq.mllib
+src/paramcoq_mod.ml: src/paramcoq.mlpack
 	sed -e "s/\([^ ]\{1,\}\)/let _=Mltop.add_known_module\"\1\" /g" $< > $@
 	echo "let _=Mltop.add_known_module\"paramcoq\"" >> $@
 

src/abstraction.ml4

@@ -16,11 +16,13 @@
 (*i camlp4deps: "src/parametricity.cmo" "src/declare_translation.cmo" i*)
 
 DECLARE PLUGIN "parametricity"
-open Parametricity
-open Declare_translation
+
+open Ltac_plugin
 open Feedback
-open Constrarg
 open Stdarg
+open Tacarg
+open Parametricity
+open Declare_translation
 
 VERNAC COMMAND EXTEND SetParametricityTactic CLASSIFIED AS SIDEFF
 | [ "Parametricity" "Tactic" ":=" tactic(t) ] -> [