diff --git a/_CoqProject.in b/_CoqProject.in
index a368a3cd..d3fbefb0 100644
--- a/_CoqProject.in
+++ b/_CoqProject.in
@@ -67,6 +67,7 @@ theories/Tactics/Help.v
 theories/Tactics/Induction.v
 theories/Tactics/ItHolds.v
 theories/Tactics/ItSuffices.v
+theories/Tactics/Specialize.v
 theories/Tactics/Take.v
 theories/Tactics/ToShow.v
 theories/Tactics/Unfold.v
@@ -137,6 +138,7 @@ tests/tactics/Either.v
 tests/tactics/Induction.v
 tests/tactics/ItHolds.v
 tests/tactics/ItSuffices.v
+tests/tactics/Specialize.v
 tests/tactics/Take.v
 tests/tactics/ToShow.v
 tests/tactics/Unfold.v
diff --git a/src/databases.mlg b/src/databases.mlg
index 8219e95e..2b94763d 100644
--- a/src/databases.mlg
+++ b/src/databases.mlg
@@ -16,7 +16,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-DECLARE PLUGIN "coq-waterproof.databases"
+DECLARE PLUGIN "coq-waterproof.plugin"
 
 {
 
@@ -73,4 +73,4 @@ VERNAC COMMAND EXTEND DatabaseQuery CLASSIFIED AS QUERY
       Feedback.msg_notice ((str "Decidability databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Decidability));
       Feedback.msg_notice ((str "Shorten databases :") ++ List.fold_left (fun acc database_name -> acc ++ str " " ++ str database_name) (str "") (get_current_databases Shorten))
     }
-END
\ No newline at end of file
+END
diff --git a/tests/libs/Analysis/StrongInductionIndexSequence.v b/tests/libs/Analysis/StrongInductionIndexSequence.v
index 41d8e005..7d8d4e78 100644
--- a/tests/libs/Analysis/StrongInductionIndexSequence.v
+++ b/tests/libs/Analysis/StrongInductionIndexSequence.v
@@ -57,38 +57,40 @@ Abort.
 
 
 
-(* Test 3:  more complicated example from actual exercises,
-    i.e. with function notation 'n(k)' and 'P(n(k)) = blue' as property. *)
+(* Test 3:  more complicated example inspired by actual exercises,
+    i.e. with function notation 'n(k)' and 'candy_seq(n(k)) = sweet' as property. *)
 Require Import Waterproof.Notations.
 Require Import Waterproof.Automation.
 
 Waterproof Enable Automation RealsAndIntegers.
 Waterproof Enable Automation Intuition.
 
-Inductive Color : Set :=
-| blue : Color
-| orange : Color.
+Inductive Flavor : Set :=
+| sweet : Flavor
+| sour  : Flavor
+| salty : Flavor.
 
-#[local] Parameter P : ℕ → Color.
-Parameter infinitely_many_blues : ∀ k : ℕ, ∃ m : ℕ, (m ≥ k)%nat ∧ P(m) = blue.
 
-Lemma exercise_10_7_6 : 
-  ∃ n : ℕ → ℕ, (is_index_seq n) ∧ (∀ k : ℕ, P (n k) = blue).
+#[local] Parameter candy_seq : ℕ → Flavor.
+Parameter infinitely_many_sweet : ∀ k : ℕ, ∃ m : ℕ, (m ≥ k)%nat ∧ candy_seq(m) = sweet.
+
+Goal
+  ∃ n : ℕ → ℕ, (is_index_seq n) ∧ (∀ k : ℕ, candy_seq (n k) = sweet).
 Proof.
 Define the index sequence n inductively.
-- By (infinitely_many_blues) it holds that
-    (∃ m : ℕ, (m ≥ 0)%nat ∧ P(m) = blue).
+- By (infinitely_many_sweet) it holds that
+    (∃ m : ℕ, (m ≥ 0)%nat ∧ candy_seq(m) = sweet).
   Obtain such an m.
   Choose n_0 := m.
-  We conclude that (P(n_0) = blue).
+  We conclude that (candy_seq(n_0) = sweet).
 - Take k : ℕ and assume n(0),...,n(k) are defined.
-  Assume that (∀ l : ℕ, (l ≤ k)%nat ⇒ P(n(l)) = blue).
+  Assume that (∀ l : ℕ, (l ≤ k)%nat ⇒ candy_seq(n(l)) = sweet).
   Assume that (∀ l : ℕ, (l < k)%nat ⇒ (n(l) < n(l+1))%nat).
-  By (infinitely_many_blues) it holds that 
-    (∃ m : ℕ, (m ≥ (n k) + 1)%nat ∧ P(m) = blue).
+  By (infinitely_many_sweet) it holds that 
+    (∃ m : ℕ, (m ≥ (n k) + 1)%nat ∧ candy_seq(m) = sweet).
   Obtain such an m.
   Choose n_kplus1 := m.
   We show both statements.
-  * We conclude that (P(n_kplus1) = blue).
+  * We conclude that (candy_seq(n_kplus1) = sweet).
   * We conclude that (n(k) < n_kplus1)%nat.
 Qed.
diff --git a/tests/tactics/Choose.v b/tests/tactics/Choose.v
index 00cab25f..25b343b6 100644
--- a/tests/tactics/Choose.v
+++ b/tests/tactics/Choose.v
@@ -59,3 +59,13 @@ Goal forall n : nat, ( ( (n = n) \/ (n + 1 = n + 1) ) -> (n + 1 = n + 1)).
     intro n.
     Fail Choose m := n.
 Abort.
+
+(** Test 5: Choose a blank *)
+Goal exists n : nat, n + 1 = n + 1.
+    Choose n := (_).
+Abort.
+
+(** Test 6: Choose a named evar *)
+Goal exists n : nat, n + 1 = n + 1.
+    Choose n := (?[m]).
+Abort.
diff --git a/tests/tactics/ItHolds.v b/tests/tactics/ItHolds.v
index 5a24c59d..33abe5ce 100644
--- a/tests/tactics/ItHolds.v
+++ b/tests/tactics/ItHolds.v
@@ -23,9 +23,9 @@ Require Import Lra.
 
 (* Set Default Timeout 1. *)
 
+Require Import Waterproof.Tactics.
 Require Import Waterproof.Automation.
 Require Import Waterproof.Notations.
-Require Import Waterproof.Tactics.
 Require Import Waterproof.Util.Assertions.
 
 Waterproof Enable Automation RealsAndIntegers.
@@ -306,6 +306,8 @@ Proof.
   By Ha it holds that B.
 Abort.
 
+(* -------------------------------------------------------------------------- *)
+
 (* Test 21: we can use "It holds that" using boolean statements *)
 Goal 1 < 2.
 Proof.
@@ -319,3 +321,63 @@ Proof.
   Since (orb true false) it holds that (1 < 2).
   assumption.
 Qed.
+
+(* -------------------------------------------------------------------------- *)
+
+(** Test 23: Test whether wrapper for specialize works *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  It holds that (6 >= 5 -> True) (i).
+Abort.
+
+(** Test 24: Test wrapper specialize blocks other tactics  *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  Fail We claim that (False).
+Abort.
+
+(** Test 25: Test wrapper specialize fails with wrong statement *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  It holds that (3 >= 5 -> True). (* test whether automation could show this*)
+  Use x := 6 in (H1).
+  Fail It holds that (3 >= 5 -> True).
+Abort.
+
+(** Test 26: Test succesful renaming hypothesis from specialize 
+  even if another instance is added inbetween. *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  assert (6 >= 5 -> True) as decoy by exact (H1 6).
+  It holds that (6 >= 5 -> True) (i).
+  ltac1:(rename i into ii). (* test for hypohtesis without producing output *)
+  Fail Check _H. (* '_H' is auto-generated by 'specialize' tactic *)
+Abort.
+
+(** Test 27: Test fail renaming hypothesis from specialize 
+  if user-specified name is already used. *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  Fail It holds that (6 >= 5 -> True) (H1).
+Abort.
+
+
+(* TODO (cf. test below): wrong statement error should have priority over wrong label. *)
+
+(** Test 28: Test fail renaming hypothesis from specialize 
+  if wrong statement user-specified name is already used. *)
+Goal (forall x : nat, x >= 5 -> True) -> True.
+Proof.
+  intro H1.
+  Use x := 6 in (H1).
+  Fail It holds that (6 >= 5 -> True) (H1).
+Abort.
diff --git a/tests/tactics/Specialize.v b/tests/tactics/Specialize.v
new file mode 100644
index 00000000..08d26cf7
--- /dev/null
+++ b/tests/tactics/Specialize.v
@@ -0,0 +1,98 @@
+(******************************************************************************)
+(*                  This file is part of Waterproof-lib.                      *)
+(*                                                                            *)
+(*   Waterproof-lib is free software: you can redistribute it and/or modify   *)
+(*    it under the terms of the GNU General Public License as published by    *)
+(*     the Free Software Foundation, either version 3 of the License, or      *)
+(*                    (at your option) any later version.                     *)
+(*                                                                            *)
+(*     Waterproof-lib is distributed in the hope that it will be useful,      *)
+(*      but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*       MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the         *)
+(*               GNU General Public License for more details.                 *)
+(*                                                                            *)
+(*     You should have received a copy of the GNU General Public License      *)
+(*   along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>.  *)
+(*                                                                            *)
+(******************************************************************************)
+
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Message.
+
+Require Import Waterproof.Tactics.
+Require Import Waterproof.Automation.
+
+(** Test 0: This should be the expected behavior. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := 3 in (H).
+It holds that (3 = 3).
+Abort.
+
+(** Test 1: This should fail as the wrong variable name is chosen. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Fail Use m := (3) in (H).
+Abort.
+
+(** Test 2: This should fail because the wrong goal is specified. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := (3) in (H).
+Fail It holds that (True).
+Abort.
+
+(** Test 3: This should fail because first the wrapper needs to be resolved. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := (3) in (H).
+Fail exact I.
+Abort.
+
+(** It should be possible to use an outside lemma *)
+Local Parameter F : nat -> nat.
+Local Parameter F_identity : forall n : nat, F n = n.
+
+Goal True.
+Proof.
+Fail It holds that (F 3 = 3).
+Use n := (5) in (F_identity).
+It holds that (F 5 = 5).
+Abort.
+
+(** Test 4: cannot use specialize tactic for function, 
+  throw readable error message stating as much.  *)
+Definition f : nat -> nat := fun (n : nat) => n.
+Goal False.
+Proof.
+  Fail Use n := 5 in (f).
+Abort.
+
+(** Test 5: original universal quantifier hypohtesis left unchanged. *)
+Goal (forall n : nat, n = n) -> True.
+Proof.
+intro H.
+Use n := 3 in (H).
+ltac1:(rename H into HH).   (* test for hypohtesis without producing output *)
+Abort.
+
+(** Test 6: multiple variable specifications  *)
+Goal (forall n m : nat, n = m) -> False.
+Proof.
+intro H.
+Use n := 3, m := 4 in (H).
+It holds that (3 = 4).
+Abort.
+
+(** Test 7: multiple variable specifications, different order  *)
+Goal (forall n m : nat, n = m) -> False.
+Proof.
+intro H.
+Use m := 4, n := 3 in (H).
+Fail It holds that (4 = 3). (* as expected :) *)
+It holds that (3 = 4).
+Abort.
diff --git a/theories/Automation/Framework.v b/theories/Automation/Framework.v
index d7b2c0b6..99c148fa 100644
--- a/theories/Automation/Framework.v
+++ b/theories/Automation/Framework.v
@@ -17,4 +17,4 @@
 (******************************************************************************)
 
 From Ltac2 Require Import Init.
-Declare ML Module "waterproof:coq-waterproof.databases".
\ No newline at end of file
+Declare ML Module "waterproof:coq-waterproof.plugin".
diff --git a/theories/Tactics.v b/theories/Tactics.v
index 65703147..3c71b81f 100644
--- a/theories/Tactics.v
+++ b/theories/Tactics.v
@@ -33,6 +33,7 @@ Require Export Tactics.Help.
 Require Export Tactics.Induction.
 Require Export Tactics.ItHolds.
 Require Export Tactics.ItSuffices.
+Require Export Tactics.Specialize.
 Require Export Tactics.Take.
 Require Export Tactics.ToShow.
 Require Export Tactics.Unfold.
diff --git a/theories/Tactics/Choose.v b/theories/Tactics/Choose.v
index 7fbb0270..9c58859e 100644
--- a/theories/Tactics/Choose.v
+++ b/theories/Tactics/Choose.v
@@ -22,6 +22,9 @@ Require Import Ltac2.Message.
 Require Import Util.Goals.
 Require Import Util.MessagesToUser.
 
+Local Ltac2 concat_list (ls : message list) : message :=
+  List.fold_right concat (of_string "") ls.
+
 (* Ltac2 Type exn ::= [ ChooseError(string) ]. *)
 
 
@@ -44,9 +47,13 @@ Require Import Util.MessagesToUser.
 Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
   lazy_match! goal with
     | [ |- exists _ : _, _] =>
-      pose ($s := $t);
+      set ($s := $t);
       let v := Control.hyp s in
       let w := Fresh.fresh (Fresh.Free.of_goal ()) @_defeq in
+      match Constr.has_evar t with
+      |  true => warn (concat_list [of_string "Please come back to this line later to make a definite choice for "; of_ident s; of_string "."])
+      | _ => ()
+      end;
       exists $v;
       assert ($w : $v = $t) by reflexivity
     | [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
@@ -68,14 +75,17 @@ Ltac2 choose_variable_in_exists_goal_with_renaming (s:ident) (t:constr) :=
 *)
 Ltac2 choose_variable_in_exists_no_renaming (t:constr) :=
     lazy_match! goal with
-        | [ |- exists _ : _, _] => exists $t
+        | [ |- exists _ : _, _] =>
+          match Constr.has_evar t with
+          |  true => warn (concat_list [of_string "Please come back to this line later to make a definite choice."]); eexists $t
+          |  false => exists $t
+          end
         | [ |- _ ] => throw (of_string "`Choose` can only be applied to 'exists' goals.")
     end.
 
-Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(constr) :=
+Ltac2 Notation "Choose" s(opt(seq(ident, ":="))) t(open_constr) :=
   panic_if_goal_wrapped ();
   match s with 
     | None => choose_variable_in_exists_no_renaming t
     | Some s => choose_variable_in_exists_goal_with_renaming s t
   end.
-
diff --git a/theories/Tactics/ItHolds.v b/theories/Tactics/ItHolds.v
index 8bbe93d6..19425512 100644
--- a/theories/Tactics/ItHolds.v
+++ b/theories/Tactics/ItHolds.v
@@ -106,6 +106,25 @@ Local Ltac2 wp_assert_by (claim : constr) (label : ident option) (xtr_lemma : co
 Local Ltac2 wp_assert_since (claim : constr) (label : ident option) (xtr_claim : constr) :=
   since_framework (core_wp_assert_by claim label) xtr_claim.
 
+(**
+  Removes a [StateHyp.Wrapper] wrapper from the goal.
+    
+  Arguments: The statement in the specified hypothesis
+    
+  Does: 
+    - Removes the wrapper [StateHyp.Wrapper A G].
+
+  Raises exception:
+    - (fatal) if the wrong hypothesis is specified.
+*)
+Local Ltac2 unwrap_state_hyp (statement : constr) :=
+  lazy_match! goal with
+    | [|- StateHyp.Wrapper ?s _] => 
+         if check_constr_equal s statement
+           then apply (StateHyp.wrap $s)
+           else throw (of_string "Wrong statement specified.")
+    | [|- _] => ()
+  end.
 
 (**
   Attempts to assert a claim and proves it automatically using a specified lemma, 
@@ -141,6 +160,32 @@ Ltac2 Notation "Since" xtr_claim(constr) "it" "holds" "that" claim(constr) label
     - (fatal) if [rwaterprove] fails to prove the claim using the specified lemma.
     - [[label] is already used], if there is already another hypothesis with identifier [label].
 *)
+
+Local Ltac2 wp_assert_with_unwrap (claim : constr) (label : ident option) :=
+  (* Try out label first. 
+    Code results in wrong error if done inside repeated match.. *)
+  match label with | None => () | Some label => try_out_label label end;
+  
+  match! goal with
+  | [h : ?s |- StateHyp.Wrapper ?s ?h_spec _] => 
+    let h_constr := Control.hyp h in
+    (* sanity check "h = h_spec" *)
+    if check_constr_equal h_constr h_spec
+      then ()
+      else fail;
+
+    if check_constr_equal s claim
+      then apply (StateHyp.wrap $s)
+      else throw (of_string "Wrong statement specified.");
+    (* rename ident generated in specialize with user-specified label*)
+    match label with
+    | None => ()
+    | Some label => Std.rename [(h, label)]
+    end
+  | [|- _] => 
+    panic_if_goal_wrapped ();
+    wp_assert claim label
+  end.
+
 Ltac2 Notation "It" "holds" "that" claim(constr) label(opt(seq("(", ident, ")")))  :=
-  panic_if_goal_wrapped ();
-  wp_assert claim label.
\ No newline at end of file
+  wp_assert_with_unwrap claim label.
\ No newline at end of file
diff --git a/theories/Tactics/Specialize.v b/theories/Tactics/Specialize.v
new file mode 100644
index 00000000..61ac281b
--- /dev/null
+++ b/theories/Tactics/Specialize.v
@@ -0,0 +1,74 @@
+(******************************************************************************)
+(*                  This file is part of Waterproof-lib.                      *)
+(*                                                                            *)
+(*   Waterproof-lib is free software: you can redistribute it and/or modify   *)
+(*    it under the terms of the GNU General Public License as published by    *)
+(*     the Free Software Foundation, either version 3 of the License, or      *)
+(*                    (at your option) any later version.                     *)
+(*                                                                            *)
+(*     Waterproof-lib is distributed in the hope that it will be useful,      *)
+(*      but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*       MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the         *)
+(*               GNU General Public License for more details.                 *)
+(*                                                                            *)
+(*     You should have received a copy of the GNU General Public License      *)
+(*   along with Waterproof-lib. If not, see <https://www.gnu.org/licenses/>.  *)
+(*                                                                            *)
+(******************************************************************************)
+
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Message.
+
+Require Import Util.Init.
+Require Import Util.Goals.
+Require Import Util.MessagesToUser.
+
+
+(**
+  Specializes a hypothesis that starts with a for-all statement.
+    
+  Arguments:
+    - [s : ident], name of the variable to choose
+    - [choice : constr], choice for the variable
+    - [in_hyp : ident], name of the hypothesis to specialize.
+
+  Raises fatal exceptions:
+    - If the hypothesis [in_hyp] does not start with a for-all statement.
+*)
+
+Local Ltac2 _ident_to_hyp_list (ls : (ident * constr) list) : (Std.hypothesis * constr) list 
+:= List.map (fun (i, x) => (Std.NamedHyp i, x)) ls.
+
+Local Ltac2 wp_specialize (var_choice_list : (ident * constr) list) (h:constr) :=
+  (* let h := Control.hyp in_hyp in *)
+  (* let named_hyp := Std.NamedHyp s in *)
+  let statement := eval unfold type_of in (type_of $h) in
+  (* let specialized_statement := eval unfold type_of in (type_of ($h $choice)) in *)
+  lazy_match! statement with
+    | _ -> ?x => (* Exclude matching on functions (naming codomain necessary) *)
+      throw (of_string "`Pick ... in (*)` only works if (*) starts with a for-all quantifier.")
+    | forall _ : _, _ =>
+      let w := Fresh.fresh (Fresh.Free.of_goal ()) @_H in
+      Std.specialize (h, Std.ExplicitBindings (_ident_to_hyp_list var_choice_list)) 
+        (Some (Std.IntroNaming (Std.IntroIdentifier w))) ;
+      (* specialize $h with ($named_hyp := $choice) as $w; *)
+      (* Wrap the goal *)
+      let constr_w := Control.hyp w in
+      let type_w := Constr.type constr_w in
+      apply (StateHyp.unwrap $type_w $constr_w)
+    | _ => throw (of_string "`Pick ... in (*)` only works if (*) starts with a for-all quantifier.")
+  end.
+
+(**
+  Specializes a hypothesis that starts with a for-all statement.
+    
+  Arguments:
+    - [s : ident], name of the variable to choose
+    - [choice : constr], choice for the variable
+    - [in_hyp : ident], name of the hypothesis to specialize.
+
+  Raises fatal exceptions:
+    - If the hypothesis [in_hyp] does not start with a for-all statement.
+*)
+Ltac2 Notation "Use" s(list1(seq(ident, ":=", constr), ",")) "in" "(" in_hyp(constr) ")" :=
+  wp_specialize s in_hyp.
diff --git a/theories/Util/Goals.v b/theories/Util/Goals.v
index 26c06969..2822b741 100644
--- a/theories/Util/Goals.v
+++ b/theories/Util/Goals.v
@@ -96,6 +96,23 @@ Notation "'Add' 'the' 'following' 'line' 'to' 'the' 'proof:' 'We' 'need' 'to' 's
     format "'[ ' Add  the  following  line  to  the  proof: ']' '//'   We  need  to  show  that  ( G ). '//' or  write: '//'   We  conclude  that  ( G ). '//' if  no  intermediary  proof  steps  are  required."
   ).
 
+Module StateHyp.
+
+  Private Inductive Wrapper (A : Type) (h : A) (G : Type) : Type :=
+    | wrap : G -> Wrapper A h G.
+
+  Definition unwrap (A : Type) (h : A) (G : Type) : Wrapper A h G -> G :=
+    fun x => match x with wrap _ _ _ y => y end.
+
+End StateHyp.
+
+Notation "'Add' 'the' 'following' 'line' 'to' 'the' 'proof:' 'It' 'holds' 'that' '(' A ').'" :=
+  (StateHyp.Wrapper A _ _) (
+    at level 99,
+    only printing,
+    format "'[ ' Add  the  following  line  to  the  proof: ']' '//'   It  holds  that  ( A )."
+  ).
+
 Module ByContradiction.
 
   Private Inductive Wrapper (A G : Type) : Type :=
@@ -147,6 +164,7 @@ Ltac2 panic_if_goal_wrapped () :=
     | [|- NaturalInduction.Base.Wrapper _] => raise_goal_wrapped_error ()
     | [|- NaturalInduction.Step.Wrapper _] => raise_goal_wrapped_error ()
     | [|- StateGoal.Wrapper _]             => raise_goal_wrapped_error ()
+    | [|- StateHyp.Wrapper _ _ _]              => raise_goal_wrapped_error ()
     | [|- ByContradiction.Wrapper _ _]     => raise_goal_wrapped_error ()
     | [|- _] => ()
   end.
diff --git a/theories/Waterproof.v b/theories/Waterproof.v
index 644e59ae..99c148fa 100644
--- a/theories/Waterproof.v
+++ b/theories/Waterproof.v
@@ -17,4 +17,4 @@
 (******************************************************************************)
 
 From Ltac2 Require Import Init.
-Declare ML Module "waterproof:coq-waterproof.plugin".
\ No newline at end of file
+Declare ML Module "waterproof:coq-waterproof.plugin".