diff options
| author | Enrico Tassi | 2020-10-13 15:32:54 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2020-11-02 10:05:17 +0100 |
| commit | 7de7fe612ffc5a598311f9542e57e50803ff2007 (patch) | |
| tree | 282e882f6f9b8ebd99ee627d0c1c26a728148104 /vernac/comDefinition.ml | |
| parent | bd4d20106589562b12186ac2d02a665cf7b49dbe (diff) | |
[doc] attribute #[using]
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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 |
