Merge pull request #10 from palmskog/fix-license-opam

Unambiguously state MIT license

Author: Matafou

LibHyps/LibHypsNaming.v

@@ -2,11 +2,6 @@
   This file is part of LibHyps. It is distributed under the MIT
   "expat license". You should have recieved a LICENSE file with it. *)
 
-(**************************************************************************
-* A user-customizable auto-naming scheme for hypothesis in Coq            *
-* Author: Pierre Courtieu                                                 *
-* Distributed under the terms of the LGPL-v3 license                      *
-***************************************************************************)
 Require Import Arith ZArith List LibHyps.TacNewHyps.
 Import ListNotations.
 Local Open Scope list.

coq-libhyps.opam

@@ -0,0 +1,48 @@
+# this is a mirror of an opam description file in the
+# opam-coq-archive at:
+# https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-libhyps
+# the latter being official and probably more up to date.
+
+opam-version: "2.0"
+maintainer: "[email protected]"
+synopsis: "Hypotheses manipulation library"
+
+homepage: "https://github.com/Matafou/LibHyps"
+dev-repo: "git+https://github.com/Matafou/LibHyps.git"
+bug-reports: "https://github.com/Matafou/LibHyps/issues"
+doc: "https://github.com/Matafou/LibHyps/blob/master/Demo/demo.v"
+license: "MIT"
+
+build: [
+  ["./configure.sh"]
+  [make "-j%{jobs}%"]
+]
+
+install: [make "install"]
+
+depends: [
+  "coq" {(>= "8.11" & < "8.17~") | (= "dev")}
+]
+
+tags: [
+  "keyword:proof environment manipulation"
+  "keyword:forward reasoning"
+  "keyword:hypothesis naming"
+  "category:Miscellaneous/Coq Tactics Library"
+  "logpath:LibHyps"
+]
+
+authors: [
+ "Pierre Courtieu"
+]
+
+description: "
+This library defines a set of tactics to manipulate hypothesis
+individually or by group. In particular it allows applying a tactic on
+each hypothesis of a goal, or only on *new* hypothesis after some
+tactic. Examples of manipulations: automatic renaming, subst, revert,
+or any tactic expecting a hypothesis name as argument.
+
+It also provides the especialize tactic to ease forward reasoning by
+instantianting one, several or all premisses of a hypothesis.
+"