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

4 files changed, 29 insertions, 11 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1c9875718..59c239bb6 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 9bbd0b8f4..345b3dc4e 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 ea5506969..9dc5cdcd7 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 51acc840e..0d0db36ce 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