Derive plugin: code reorganisation for clarity.

1 files changed, 36 insertions, 38 deletions

diff --git a/plugins/Derive/derive.ml b/plugins/Derive/derive.ml
index fbf7131e67..41fb3985e7 100644
--- a/plugins/Derive/derive.ml
+++ b/plugins/Derive/derive.ml
@@ -37,47 +37,45 @@ let start_deriving f suchthat lemma =
     in
     let terminator com =
       let open Proof_global in
-      match com with
-      | Admitted -> Errors.error"Admitted isn't supported in Derive."
-      | Proved (_,Some _,_) ->
-          Errors.error"Cannot save a proof of Derive with an explicit name."
-      | Proved (opaque, None, obj) ->
-          let (f_def,lemma_def) =
+      let (opaque,f_def,lemma_def) =
+        match com with
+        | Admitted -> Errors.error"Admitted isn't supported in Derive."
+        | Proved (_,Some _,_) ->
+            Errors.error"Cannot save a proof of Derive with an explicit name."
+        | Proved (opaque, None, obj) ->
             match Proof_global.(obj.entries) with
             | [_;f_def;lemma_def] ->
-                f_def , lemma_def
+                opaque , f_def , lemma_def
             | _ -> assert false
-          in
-          (* The opacity of [f_def] is adjusted to be [false]. *)
-          let f_def = let open Entries in { f_def with
-          const_entry_opaque = false ; }
-        in
-        let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
-        let f_kn = Declare.declare_constant f f_def in
-        let f_kn_term = Term.mkConst f_kn in
-        let substf c = Vars.replace_vars [f,f_kn_term] c in
-        let lemma_pretype =
-          match Entries.(lemma_def.const_entry_type) with
-          | Some t -> t
-          | None -> assert false (* Proof_global always sets type here. *)
-        in
-        (* substitutes the variable [f] by the constant [f] it was standing for. *)
-        let lemma_type = substf lemma_pretype in
-        (* The type of [lemma_def] is adjusted to refer to [f_kn], the
-           opacity is adjusted by the proof ending command.  *)
-        let lemma_body =
-          map_const_entry_body substf Entries.(lemma_def.const_entry_body)
-        in
-        let lemma_def = let open Entries in { lemma_def with
-          const_entry_body = lemma_body ;
-          const_entry_type = Some lemma_type ;
-          const_entry_opaque = opaque ; }
-        in
-        let lemma_def =
-          Entries.DefinitionEntry lemma_def ,
-          Decl_kinds.(IsProof Proposition)
-        in
-        ignore (Declare.declare_constant lemma lemma_def)
+      in
+      (* The opacity of [f_def] is adjusted to be [false]. *)
+      let f_def = { f_def with Entries.const_entry_opaque = false } in
+      let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
+      let f_kn = Declare.declare_constant f f_def in
+      let f_kn_term = Term.mkConst f_kn in
+      let substf c = Vars.replace_vars [f,f_kn_term] c in
+      let lemma_pretype =
+        match Entries.(lemma_def.const_entry_type) with
+        | Some t -> t
+        | None -> assert false (* Proof_global always sets type here. *)
+      in
+      (* substitutes the variable [f] by the constant [f] it was standing for. *)
+      let lemma_type = substf lemma_pretype in
+      (* The type of [lemma_def] is adjusted to refer to [f_kn], the
+         opacity is adjusted by the proof ending command.  *)
+      let lemma_body =
+        map_const_entry_body substf Entries.(lemma_def.const_entry_body)
+      in
+      let lemma_def = let open Entries in { lemma_def with
+        const_entry_body = lemma_body ;
+        const_entry_type = Some lemma_type ;
+        const_entry_opaque = opaque ; }
+      in
+      let lemma_def =
+        Entries.DefinitionEntry lemma_def ,
+        Decl_kinds.(IsProof Proposition)
+      in
+      ignore (Declare.declare_constant lemma lemma_def)
   in
   let () = Proof_global.start_dependent_proof lemma kind goals terminator in
   let _ = Proof_global.with_current_proof begin fun _ p ->