poursuite de Vernacentries

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

4 files changed, 47 insertions, 16 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 067274aa73..7dca2b1c8a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -22,18 +22,29 @@ let make_strength = function
   | [] -> NeverDischarge
   | l  -> DischargeAt (sp_of_wd l)
 
+let make_strength_0 () = make_strength (Lib.cwd())
+
+let make_strength_1 () =
+  let path = try List.tl (List.tl (Lib.cwd())) with Failure _ -> [] in
+  make_strength path
+
+let make_strength_2 () =
+  let path = try List.tl (Lib.cwd()) with Failure _ -> [] in
+  make_strength path
+
+
 (* Variables. *)
 
-type variable_declaration = identifier * constr * strength * bool
+type variable_declaration = constr * strength * bool
 
-let vartab = ref (Spmap.empty : variable_declaration Spmap.t)
+let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 
 let _ = Summary.declare_summary "VARIABLE"
 	  { Summary.freeze_function = (fun () -> !vartab);
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,((id,ty,_,_) as vd)) = 
+let cache_variable (sp,(id,(ty,_,_) as vd)) = 
   Global.push_var (id,ty);
   Nametab.push id sp;
   vartab := Spmap.add sp vd !vartab
@@ -55,9 +66,9 @@ let (in_variable, out_variable) =
     specification_function = specification_variable } in
   declare_object ("VARIABLE", od)
 
-let declare_variable ((id,ty,_,_) as obj) =
+let declare_variable id ((ty,_,_) as obj) =
   Global.push_var (id,ty);
-  let sp = add_leaf id CCI (in_variable obj) in
+  let sp = add_leaf id CCI (in_variable (id,obj)) in
   Nametab.push id sp
 
 (* Parameters. *)
@@ -86,7 +97,7 @@ let declare_parameter id c =
  
 (* Constants. *)
 
-type constant_declaration = identifier * constant_entry * strength * bool
+type constant_declaration = constant_entry * strength * bool
 
 let csttab = ref (Spmap.empty : constant_declaration Spmap.t)
 
@@ -114,7 +125,7 @@ let (in_constant, out_constant) =
     specification_function = specification_constant } in
   declare_object ("CONSTANT", od)
 
-let declare_constant ((id,ce,_,_) as cd) =
+let declare_constant id ((ce,_,_) as cd) =
   let sp = add_leaf id CCI (in_constant ce) in
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
@@ -204,13 +215,13 @@ let is_variable id =
   let sp = Nametab.sp_of_id CCI id in Spmap.mem sp !vartab
   
 let out_variable sp = 
-  let (id,_,str,sticky) = Spmap.find sp !vartab in
+  let (id,(_,str,sticky)) = Spmap.find sp !vartab in
   let (_,ty) = Global.lookup_var id in
   (id,ty,str,sticky)
 
 let variable_strength id =
   let sp = Nametab.sp_of_id CCI id in 
-  let (_,_,str,_) = Spmap.find sp !vartab in
+  let _,(_,str,_) = Spmap.find sp !vartab in
   str
 
 (* Global references. *)
@@ -293,8 +304,8 @@ let declare_eliminations sp =
   let redmind = minductype_spec env sigma mind in
   let mindstr = string_of_id mindid in
   let declare na c =
-    declare_constant 
-      (id_of_string na, { const_entry_body = c; const_entry_type = None },
+    declare_constant (id_of_string na)
+      ({ const_entry_body = c; const_entry_type = None },
        false, NeverDischarge)
   in
   let mispec = Global.lookup_mind_specif redmind in 
diff --git a/library/declare.mli b/library/declare.mli
index 952fa0500b..1a9a0fac21 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -20,14 +20,14 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
-type variable_declaration = identifier * constr * strength * bool
+type variable_declaration = constr * strength * bool
 
-val declare_variable : variable_declaration -> unit
+val declare_variable : identifier -> variable_declaration -> unit
 
 
-type constant_declaration = identifier * constant_entry * strength * bool
+type constant_declaration = constant_entry * strength * bool
 
-val declare_constant : constant_declaration -> unit
+val declare_constant : identifier -> constant_declaration -> unit
 
 val declare_parameter : identifier -> constr -> unit
 
@@ -41,6 +41,9 @@ val declare_eliminations : section_path -> unit
 val declare_syntax_constant : identifier -> constr -> unit
 
 val make_strength : string list -> strength
+val make_strength_0 : unit -> strength
+val make_strength_1 : unit -> strength
+val make_strength_2 : unit -> strength
 
 (*s Corresponding test and access functions. *)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 2cc34c3cb4..cd9a5ef4e1 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -15,6 +15,21 @@ type implicits =
 
 let implicit_args = ref false
 
+let make_implicit_args flag = implicit_args := flag
+let is_implicit_args () = !implicit_args
+
+let implicitely f x =
+  let oimplicit = !implicit_args in
+  try 
+    implicit_args := true;
+    let rslt = f x in 
+    implicit_args := oimplicit;
+    rslt
+  with e -> begin
+    implicit_args := oimplicit;
+    raise e
+  end
+
 let auto_implicits ty =
   if !implicit_args then
     let genv = Global.env() in
diff --git a/library/impargs.mli b/library/impargs.mli
index 51ada5845a..8a598ef7e8 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -14,7 +14,9 @@ type implicits =
   | Impl_manual of int list
   | No_impl
 
-val implicit_args : bool ref
+val make_implicit_args : bool -> unit
+val is_implicit_args : unit -> bool
+val implicitely : ('a -> 'b) -> 'a -> 'b
 
 val list_of_implicits : implicits -> int list