[vernac] Nit refatoring on lemma command interpretation

1 files changed, 25 insertions, 19 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index cbf43127ca..f1ffb947c1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -490,12 +490,32 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
-(* Checks for start_lemma_com *)
+(* XXX: Interpretation of lemma command, duplication with ComFixpoint
+   / ComDefinition ? *)
+let interp_lemma ~program_mode ~flags ~scope env0 evd thms =
+  let inference_hook = if program_mode then Some program_inference_hook else None in
+  List.fold_left_map (fun evd ((id, _), (bl, t)) ->
+      let evd, (impls, ((env, ctx), imps)) =
+        Constrintern.interp_context_evars ~program_mode env0 evd bl
+      in
+      let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
+      let flags = Pretyping.{ all_and_fail_flags with program_mode } in
+      let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
+      let ids = List.map Context.Rel.Declaration.get_name ctx in
+      check_name_freshness scope id;
+      let thm = { Declare.Recthm.name = id.CAst.v
+                ; typ = EConstr.it_mkProd_or_LetIn t' ctx
+                ; args = ids; impargs = imps @ imps' } in
+      evd, thm)
+    evd thms
+
+(* Checks done in start_lemma_com *)
 let post_check_evd ~udecl ~poly evd =
   let () =
-    let open UState in
-    if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
-      ignore (Evd.check_univ_decl ~poly evd udecl) in
+    if not UState.(udecl.univdecl_extensible_instance &&
+                   udecl.univdecl_extensible_constraints) then
+      ignore (Evd.check_univ_decl ~poly evd udecl)
+  in
   if poly then evd
   else (* We fix the variables to ensure they won't be lowered to Set *)
     Evd.fix_undefined_variables evd
@@ -505,21 +525,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
-  let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
-    let evd, (impls, ((env, ctx), imps)) =
-      Constrintern.interp_context_evars ~program_mode env0 evd bl
-    in
-    let evd, (t', imps') = Constrintern.interp_type_evars_impls ~flags ~impls env evd t in
-    let flags = Pretyping.{ all_and_fail_flags with program_mode } in
-    let inference_hook = if program_mode then Some program_inference_hook else None in
-    let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
-    let ids = List.map Context.Rel.Declaration.get_name ctx in
-    check_name_freshness scope id;
-    let thm = { Declare.Recthm.name = id.CAst.v
-              ; typ = EConstr.it_mkProd_or_LetIn t' ctx
-              ; args = ids; impargs = imps @ imps' } in
-    evd, thm)
-      evd thms in
+  let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
   let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
   match mut_analysis with