Fix mistake with comment

Author: jim-portegies

src/g_waterproof.mlg

@@ -23,50 +23,6 @@ open Exceptions
 open Waterprove
 
 let waterproof_version : string = "3.1.1+dev"
-
-(* The code below is a hack to patch in (open_)lconstr into Ltac2 *)
-(* It should be removed when merged to coq-master (open_)lconstr should be in release 9.1 *)
-let add_scope s f =
-  Ltac2_plugin.Tac2entries.register_scope (Names.Id.of_string s) f
-
-let rec pr_scope =
-  let open Ltac2_plugin.Tac2expr in
-  let open CAst in function
-    | SexprStr {v=s; _} -> Pp.qstring s
-    | SexprInt {v=n; _} -> Pp.int n
-    | SexprRec (_, {v=na; _}, args) ->
-      let na = match na with
-        | None -> Pp.str "_"
-        | Some id -> Names.Id.print id
-      in
-      Pp.(na ++ str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")")
-
-let scope_fail s args =
-  let open Pp in
-  let args = str "(" ++ prlist_with_sep (fun () -> str ", ") pr_scope args ++ str ")" in
-  CErrors.user_err (str "Invalid arguments " ++ args ++ str " in scope " ++ str s)
-
-let () = add_scope "lconstr" (fun arg ->
-  let delimiters = List.map (function
-      | Ltac2_plugin.Tac2expr.SexprRec (_, { v = Some s; _ }, []) -> s
-      | _ -> scope_fail "lconstr" arg)
-      arg
-  in
-  let act e = Ltac2_plugin.Tac2quote.of_constr ~delimiters e in
-  Ltac2_plugin.Tac2entries.ScopeRule (Procq.Symbol.nterm Procq.Constr.lconstr, act)
-  )
-
-let () = add_scope "open_lconstr" (fun arg ->
-  let delimiters = List.map (function
-      | Ltac2_plugin.Tac2expr.SexprRec (_, { v = Some s; _ }, []) -> s
-      | _ -> scope_fail "open_.constr" arg)
-      arg
-  in
-  let act e = Ltac2_plugin.Tac2quote.of_open_constr ~delimiters e in
-  Ltac2_plugin.Tac2entries.ScopeRule (Procq.Symbol.nterm Procq.Constr.lconstr, act)
-  )
-(* End of hack *)
-*)
 }
 
 (* Add any words that occur right after mathematical expressions as keywords *)