Verilog OCaml Emacs Lisp
Fetching latest commit…
Cannot retrieve the latest commit at this time.
|Failed to load latest commit information.|
Case_Tactics: a variation on the (S*)Case tactics by Aaron Bohannon =================================== Copyright 2010 Alexandre Pilkiewicz (email@example.com) Adapted form the Constructors plugin by Matthieu Sozeau https://github.com/mattam82/Constructors Copyright 2010 Matthieu Sozeau <firstname.lastname@example.org>. All rights reserved. ML module distributed under the terms of the GNU Lesser General Public License Version 2.1, see LICENSE for details. Coq files in public domain (WTF Public Licence) The archive has 3 subdirectories: src/ contains the code of the plugin in case_tactics.ml and a support file for building the case_tactics plugin. theories/ contains support Coq file for the plugin. Case_Tactics.v declares the plugin on the Coq side. test-suite/ demonstrates a use of the plugin. It serves as documentation the file insert_case.el contains two emacs functions, insert-case and insert-all-cases that get the current Case (of (S*)Case) from the context and copy them in the development script. Just add the content to your .emacs to use it Installation ============ First, you should have coqc, ocamlc and make in your path. Then simply do: # coq_makefile -f Make -o Makefile To generate a makefile from the description in Make, then # make This will consecutively build the plugin, the supporting theories and the test-suite file. You can then either [make install] the plugin or leave it in its current directory. To be able to import it from anywhere in Coq, simply add the following to ~/.coqrc: Add Rec LoadPath "path_to_case_tactics/theories" as Case_Tactics. Add ML Path "path_to_case_tactics/src". To use it in a development, add those options to coqc -I path_to_case_tactics/src -R path_to_case_tactics/theories Case_Tactics