From 66ffe00ed59e6bfcff4d29bdef8c1c1e3a8f5a64 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Jul 2013 15:31:40 +0000
Subject: Safe_typing: minor factorisation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 636644ec3a..753b97a0c4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -507,17 +507,18 @@ let add_module_parameter mbid mte inl senv =
     anomaly (Pp.str "Cannot add a module parameter to a non empty module")
   | _ -> ()
   in
-  let mtb = translate_module_type senv.env (MPbound mbid) inl mte in
-  let senv = 
-    full_add_module (module_body_of_type (MPbound mbid) mtb) senv
+  let mp = MPbound mbid in
+  let mtb = translate_module_type senv.env mp inl mte in
+  let senv = full_add_module (module_body_of_type mp mtb) senv
   in
   let new_variant = match senv.modinfo.variant with
     | STRUCT params -> STRUCT ((mbid,mtb) :: params)
     | SIG params -> SIG ((mbid,mtb) :: params)
     | _ ->
-	anomaly (Pp.str "Module parameters can only be added to modules or signatures")  
+      let msg = "Module parameters can only be added to modules or signatures"
+      in anomaly (Pp.str msg)
   in
-    
+
   let resolver_of_param = match mtb.typ_expr with
       SEBstruct _ -> mtb.typ_delta
     | _ -> empty_delta_resolver
-- 
cgit v1.2.3