Mécanisme pour faire remonter les contraintes de typage sur les variables de section au niveau du discharge, sans avoir à garder tout l'environnement de la section

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 44 insertions, 15 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 482be2fb99..e8ed6ca32e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -161,4 +161,5 @@ let cook_constant env r =
   let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
   let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
   let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in
-  abstract_constant r.d_abstract hyps (body,typ)
+  let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
+  (body, typ, cb.const_constraints)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index d9b564835b..db2ba15516 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -12,6 +12,7 @@ open Names
 open Term
 open Declarations
 open Environ
+open Univ
 
 (*s Cooking the constants. *)
 
@@ -32,7 +33,7 @@ type recipe = {
   d_abstract : identifier list;
   d_modlist : work_list }
 
-val cook_constant : env -> recipe -> constr option * constr
+val cook_constant : env -> recipe -> constr option * constr * constraints
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 102fbb228e..ff1a8131d6 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -38,6 +38,13 @@ val push_named_assum :
 val push_named_def :
   identifier * constr -> safe_environment -> safe_environment
 
+val check_and_push_named_assum :
+  identifier * constr -> safe_environment ->
+    (constr option * types * constraints) * safe_environment
+val check_and_push_named_def :
+  identifier * constr -> safe_environment -> 
+    (constr option * types * constraints) * safe_environment
+
 type local_names = (identifier * variable_path) list
 
 val add_parameter :
diff --git a/library/declare.ml b/library/declare.ml
index 1c98757180..59c239bb64 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -57,9 +57,14 @@ type sticky = bool
 
 type variable_declaration = section_variable_entry * strength * sticky
 
+type checked_section_variable = constr option * types * Univ.constraints
+
+type checked_variable_declaration =
+    checked_section_variable * strength * sticky
+
 let vartab =
   ref ((Spmap.empty, []) :
-       (identifier * variable_declaration) Spmap.t * section_path list)
+       (identifier * checked_variable_declaration) Spmap.t * section_path list)
 
 let current_section_context () =
   List.map (fun sp -> (basename sp, sp)) (snd !vartab)
@@ -70,7 +75,7 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.init_function = (fun () -> vartab := (Spmap.empty, []));
 	    Summary.survive_section = false }
 
-let cache_variable (sp,(id,(d,_,_) as vd)) =
+let cache_variable (sp,(id,(d,str,sticky))) =
 (*
   if Nametab.exists_cci sp then
 *)
@@ -78,12 +83,12 @@ let cache_variable (sp,(id,(d,_,_) as vd)) =
   if List.mem_assoc id (current_section_context ()) then
     errorlabstrm "cache_variable"
       [< pr_id (basename sp); 'sTR " already exists" >];
-  begin match d with (* Fails if not well-typed *)
+  let vd = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef c -> Global.push_named_def (id,c)
-  end;
+  in
   Nametab.push_short_name sp (VarRef sp);
-  vartab := let (m,l) = !vartab in (Spmap.add sp vd m, sp::l)
+  vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str,sticky)) m, sp::l)
 
 let (in_variable, out_variable) =
   let od = {
@@ -293,10 +298,15 @@ let constant_or_parameter_strength sp =
   try constant_strength sp with Not_found -> NeverDischarge
 
 let get_variable sp = 
-  let (id,(_,str,sticky)) = Spmap.find sp (fst !vartab) in
-  let (c,ty) = Global.lookup_named id in
+  let (id,((c,ty,cst),str,sticky)) = Spmap.find sp (fst !vartab) in
+(*  let (c,ty) = Global.lookup_named id in*)
   ((id,c,ty),str,sticky)
 
+let get_variable_with_constraints sp = 
+  let (id,((c,ty,cst),str,sticky)) = Spmap.find sp (fst !vartab) in
+(*  let (c,ty) = Global.lookup_named id in*)
+  ((id,c,ty),cst,str,sticky)
+
 let variable_strength sp =
   let _,(_,str,_) = Spmap.find sp (fst !vartab) in str
 
diff --git a/library/declare.mli b/library/declare.mli
index 9bbd0b8f40..345b3dc4e0 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -78,6 +78,8 @@ val constant_or_parameter_strength : constant_path -> strength
 
 val out_variable : Libobject.obj -> identifier * variable_declaration
 val get_variable : variable_path -> named_declaration * strength * sticky
+val get_variable_with_constraints : 
+  variable_path -> named_declaration * Univ.constraints * strength * sticky
 val variable_strength : variable_path -> strength
 val find_section_variable : identifier -> variable_path
 val last_section_hyps : dir_path -> identifier list
diff --git a/library/global.ml b/library/global.ml
index ea5506969a..9dc5cdcd72 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -39,8 +39,13 @@ let universes () = universes !global_env
 let context () = context !global_env
 let named_context () = named_context !global_env
 
-let push_named_def idc = global_env := push_named_def idc !global_env
-let push_named_assum idc = global_env := push_named_assum idc !global_env
+let push_named_def idc =
+  let d, env = check_and_push_named_def idc !global_env in
+  global_env := env; d
+
+let push_named_assum idc =
+  let d, env = check_and_push_named_assum idc !global_env in
+  global_env := env; d
 
 let add_parameter sp c l = global_env := add_parameter sp c l !global_env
 let add_constant sp ce l = global_env := add_constant sp ce l !global_env
diff --git a/library/global.mli b/library/global.mli
index 51acc840ee..0d0db36cec 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -30,8 +30,9 @@ val universes : unit -> universes
 val context : unit -> context
 val named_context : unit -> named_context
 
-val push_named_assum : identifier * constr -> unit
-val push_named_def : identifier * constr -> unit
+(* This has also a side-effect to push the declaration in the environment*)
+val push_named_assum : identifier * constr -> constr option * types*constraints
+val push_named_def : identifier * constr -> constr option * types * constraints
 
 val add_parameter : section_path -> constr -> local_names -> unit
 val add_constant : section_path -> constant_entry -> local_names -> unit
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index c8e031bb86..a9c1273e85 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -171,6 +171,7 @@ type discharge_operation =
   | Objdef of constant_path
   | Coercion of coercion_entry
   | Require of module_reference
+  | Constraints of Univ.constraints
 
 (* Main function to traverse the library segment and compute the various
    discharge operations. *)
@@ -180,13 +181,13 @@ let process_object oldenv dir sec_sp
   let tag = object_tag lobj in 
   match tag with
     | "VARIABLE" ->
-	let ((id,c,t),stre,sticky) = get_variable sp in
+	let ((id,c,t),cst,stre,sticky) = get_variable_with_constraints sp in
 	(* VARIABLE means local (entry Variable/Hypothesis/Local and are *)
 	(* always discharged *)
 (*
  	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
 *)
-	  (ops,id::ids_to_discard,work_alist)
+	  (Constraints cst :: ops, id :: ids_to_discard, work_alist)
 (*
 	else
 	  let imp = is_implicit_var sp in
@@ -302,6 +303,7 @@ let process_operation = function
       begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
   | Coercion y -> add_new_coercion y
   | Require y -> reload_module y
+  | Constraints y -> Global.add_constraints y
 
 let catch_not_found f x =
   try f x