initialize project

Author: tlringer

.gitignore

@@ -0,0 +1,13 @@
+Makefile
+Makefile.conf
+*.d
+*.aux
+*.glob
+*.vo
+*.a
+*.cmi
+*.cmx
+*.cmxa
+*.cmxs
+*.o
+.merlin

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "plugin/src/coq-plugin-lib"]
+	path = plugin/src/coq-plugin-lib
+	url = https://github.com/uwplse/coq-plugin-lib.git

README.md

@@ -1 +1,13 @@
 This repository contains the `Preprocess` command by [Nate Yazdani](https://github.com/nateyazdani), which does simple match and fixpoint to eliminator translation for certain terms, as described in the [DEVOID paper](http://tlringer.github.io/pdf/ornpaper.pdf). This command is used in both [PUMPKIN PATCH](https://github.com/uwplse/PUMPKIN-PATCH) and [DEVOID](https://github.com/uwplse/ornamental-search). Here it exists as a standalone plugin so that others can build on it as desired.
+
+This plugin depends on Coq 8.8 and our Coq plugin library.
+The library is included automatically.
+To build the standalone plugin, run:
+
+```
+cd plugin
+./build.sh
+```
+
+For examples of using this plugin within another plugin,
+see [PUMPKIN PATCH](https://github.com/uwplse/PUMPKIN-PATCH) and [DEVOID](https://github.com/uwplse/ornamental-search).

plugin/_CoqProject

@@ -0,0 +1,8 @@
+-I src
+-R src Fixtranslation
+-Q theories Fixtranslation
+
+src/fixtranslation.ml4
+src/fixtoelim.mlpack
+
+theories/Fixtoelim.v

plugin/build.sh

@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+git submodule init
+git submodule update
+coq_makefile -f _CoqProject -o Makefile
+make clean && make && make install
+

plugin/src/coq-plugin-lib

@@ -0,0 +1 @@
+Fixtranslation

plugin/src/fixtoelim.mlpack

@@ -0,0 +1 @@
+DECLARE PLUGIN "fixtoelim"

plugin/src/fixtranslation.ml4

@@ -0,0 +1 @@
+Declare ML Module "fixtoelim".