From 7de7fe612ffc5a598311f9542e57e50803ff2007 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Oct 2020 15:32:54 +0200
Subject: [doc] attribute #[using]

---
 vernac/comDefinition.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'vernac/comDefinition.ml')

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index aa71e58cf6..3fc74cba5b 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -121,7 +121,8 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct
   let using = using |> Option.map (fun expr ->
     let terms = body :: match types with Some x -> [x] | None -> [] in
     let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
   let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
@@ -140,7 +141,8 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red
   let using = using |> Option.map (fun expr ->
     let terms = body :: match types with Some x -> [x] | None -> [] in
     let l = Proof_using.process_expr (Global.env()) evd expr terms in
-    Names.Id.Set.(List.fold_right add l empty)) in
+    Names.Id.Set.(List.fold_right add l empty))
+  in
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
-- 
cgit v1.2.3