From 1eaebf4ab7616b2be16b957736e80f1d6100eae0 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 9 May 2013 20:48:29 +0000
Subject: Use definition_entry to declare local definitions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/entries.mli     | 3 ++-
 kernel/safe_typing.ml  | 4 ++--
 kernel/safe_typing.mli | 2 +-
 kernel/term_typing.ml  | 6 +++---
 kernel/term_typing.mli | 2 +-
 5 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2d65d3ed3..392a2cd84f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -47,9 +47,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list }
 
 (** {6 Constants (Definition/Axiom) } *)
+type const_entry_body = constr
 
 type definition_entry = {
-  const_entry_body   : constr;
+  const_entry_body   : const_entry_body;
   const_entry_secctx : Context.section_context option;
   const_entry_type        : types option;
   const_entry_opaque      : bool;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8518036213..62e2d46a85 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -245,8 +245,8 @@ let safe_push_named (id,_,_ as d) env =
     with Not_found -> () in
   Environ.push_named d env
 
-let push_named_def (id,b,topt) senv =
-  let (c,typ,cst) = Term_typing.translate_local_def senv.env (b,topt) in
+let push_named_def (id,de) senv =
+  let (c,typ,cst) = Term_typing.translate_local_def senv.env de in
   let senv' = add_constraints cst senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46dac02aa1..31bb8143e9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -34,7 +34,7 @@ val push_named_assum :
   Id.t * types -> safe_environment ->
     Univ.constraints * safe_environment
 val push_named_def :
-  Id.t * constr * types option -> safe_environment ->
+  Id.t * definition_entry -> safe_environment ->
     Univ.constraints * safe_environment
 
 (** Adding global axioms or definitions *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 83d1ce16c4..33a4b55e87 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -42,9 +42,9 @@ let local_constrain_type env j cst1 = function
       assert (eq_constr t tj.utj_val);
       t, union_constraints (union_constraints cst1 cst2) cst3
 
-let translate_local_def env (b,topt) =
-  let (j,cst) = infer env b in
-  let (typ,cst) = local_constrain_type env j cst topt in
+let translate_local_def env de =
+  let (j,cst) = infer env de.const_entry_body in
+  let (typ,cst) = local_constrain_type env j cst de.const_entry_type in
     (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index cc6025dabe..c9bff84fc7 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -13,7 +13,7 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> constr * types option ->
+val translate_local_def : env -> definition_entry ->
   constr * types * constraints
 
 val translate_local_assum : env -> types -> types * constraints
-- 
cgit v1.2.3