Prise en compte des coercions dans les clauses "with" même si le type

de l'argument donné contient des métavariables (souhait
#1408). Beaucoup d'infrastructure autour des constantes pour cela mais
qu'on devrait pouvoir récupérer pour analyser plus finement le
comportement des constantes en général :

1- Pour insérer les coercions, on utilise une transformation
   (expérimentale) de Metas vers Evars le temps d'appeler coercion.ml.
2- Pour la compatibilité, on s'interdit d'insérer une coercion entre
   classes flexibles parce que sinon l'insertion de coercion peut prendre
   précédence sur la résolution des evars ce qui peut changer les 
   comportements (comme dans la preuve de fmg_cs_inv dans CFields de CoRN).
3- Pour se souvenir rapidement de la nature flexible ou rigide du
   symbole de tête d'une constante vis à vis de l'évaluation, on met en
   place une table associant à chaque constante sa constante de tête (heads.ml)
4- Comme la table des constantes de tête a besoin de connaître
   l'opacité des variables de section, la partie tables de declare.ml va
   dans un nouveau decls.ml.

Au passage, simplification de coercion.ml, correction de petits bugs
(l'interface de Gset.fold n'était pas assez générale; specialize 
 cherchait à typer un terme dans un mauvais contexte d'evars [tactics.ml];
 whd_betaiotazeta avait un argument env inutile [reduction.ml, inductive.ml])
 et nettoyage (declare.ml, decl_kinds.ml, avec incidence sur class.ml,
 classops.ml et autres ...; uniformisation noms tables dans autorewrite.ml).



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

9 files changed, 473 insertions, 175 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 8ea183509..20808f1e6 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -9,10 +9,11 @@
 (* $Id$ *)
 
 open Util
+open Libnames
 
 (* Informal mathematical status of declarations *)
 
-type locality_flag = (*bool (* local = true; global = false *)*)
+type locality =
   | Local
   | Global
 
@@ -40,8 +41,6 @@ type definition_object_kind =
   | IdentityCoercion
   | Instance
 
-type strength = locality_flag (* For compatibility *)
-
 type assumption_object_kind = Definitional | Logical | Conjectural
 
 (* [assumption_kind] 
@@ -52,9 +51,9 @@ type assumption_object_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality_flag * assumption_object_kind
+type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality_flag * boxed_flag * definition_object_kind
+type definition_kind = locality * boxed_flag * definition_object_kind
 
 (* Kinds used in proofs *)
 
@@ -62,7 +61,7 @@ type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality_flag * goal_object_kind
+type goal_kind = locality * goal_object_kind
 
 (* Kinds used in library *)
 
@@ -100,3 +99,13 @@ let string_of_definition_kind (l,boxed,d) =
       anomaly "Unsupported local definition kind"
   | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Instance)
       -> anomaly "Internal definition kind"
+
+(* Strength *)
+
+let strength_of_global = function
+  | VarRef _ -> Local
+  | IndRef _ | ConstructRef _ | ConstRef _ -> Global
+
+let string_of_strength = function
+  | Local -> "Local"
+  | Global -> "Global"
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
new file mode 100644
index 000000000..c9485fa5b
--- /dev/null
+++ b/library/decl_kinds.mli
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: decl_kinds.ml 10410 2007-12-31 13:11:55Z msozeau $ *)
+
+open Util
+open Libnames
+
+(* Informal mathematical status of declarations *)
+
+type locality =
+  | Local
+  | Global
+
+type boxed_flag = bool
+
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+  | Property
+  | Proposition
+  | Corollary
+
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
+  | Instance
+
+type assumption_object_kind = Definitional | Logical | Conjectural
+
+(* [assumption_kind] 
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+
+*)
+type assumption_kind = locality * assumption_object_kind
+
+type definition_kind = locality * boxed_flag * definition_object_kind
+
+(* Kinds used in proofs *)
+
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
+  | Proof of theorem_kind
+
+type goal_kind = locality * goal_object_kind
+
+(* Kinds used in library *)
+
+type logical_kind =
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
+
+(* Utils *)
+
+val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
+val string_of_theorem_kind : theorem_kind -> string
+val string_of_definition_kind :
+  locality * boxed_flag * definition_object_kind -> string
+
+(* About locality *)
+
+val strength_of_global : global_reference -> locality
+val string_of_strength : locality -> string
diff --git a/library/declare.ml b/library/declare.ml
index 278acc665..b524639ef 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -8,6 +8,8 @@
 
 (* $Id$ *)
 
+(** This module is about the low-level declaration of logical objects *)
+
 open Pp
 open Util
 open Names
@@ -17,32 +19,16 @@ open Term
 open Sign
 open Declarations
 open Entries
-open Inductive
-open Indtypes
-open Reduction
-open Type_errors
-open Typeops
 open Libobject
 open Lib
 open Impargs
-open Nametab
 open Safe_typing
+open Cooking
+open Decls
 open Decl_kinds
 
-(**********************************************)
-
-(* Strength *)
-
-open Nametab
+(** XML output hooks *)
 
-let strength_min (stre1,stre2) =
-  if stre1 = Local or stre2 = Local then Local else Global
-
-let string_of_strength = function
-  | Local -> "(local)"
-  | Global -> "(global)"
-
-(* XML output hooks *)
 let xml_declare_variable = ref (fun (sp:object_name) -> ())
 let xml_declare_constant = ref (fun (sp:bool * constant)-> ())
 let xml_declare_inductive = ref (fun (sp:bool * object_name) -> ())
@@ -53,7 +39,7 @@ let set_xml_declare_variable f = xml_declare_variable := if_xml f
 let set_xml_declare_constant f = xml_declare_constant := if_xml f
 let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
 
-(* Section variables. *)
+(** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
@@ -61,53 +47,30 @@ type section_variable_entry =
 
 type variable_declaration = dir_path * section_variable_entry * logical_kind
 
-type checked_section_variable =
-  | CheckedSectionLocalDef of constr * types * Univ.constraints * bool
-  | CheckedSectionLocalAssum of types * Univ.constraints
-
-type checked_variable_declaration = 
-    dir_path * checked_section_variable * logical_kind
-
-let vartab = ref (Idmap.empty : checked_variable_declaration Idmap.t)
-
-let _ = Summary.declare_summary "VARIABLE"
-  { Summary.freeze_function = (fun () -> !vartab);
-    Summary.unfreeze_function = (fun ft -> vartab := ft);
-    Summary.init_function = (fun () -> vartab := Idmap.empty);
-    Summary.survive_module = false;
-    Summary.survive_section = false }
-
 let cache_variable ((sp,_),o) =
   match o with
   | Inl cst -> Global.add_constraints cst
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
-  if Idmap.mem id !vartab then
+  if variable_exists id then
     errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
-  let vd,impl,keep = match d with (* Fails if not well-typed *)
+  let impl,opaq,cst,keep = match d with (* Fails if not well-typed *)
     | SectionLocalAssum (ty, impl, keep) ->
         let cst = Global.push_named_assum (id,ty) in
-        let (_,bd,ty) = Global.lookup_named id in
-        CheckedSectionLocalAssum (ty,cst), impl, if keep then Some ty else None
+        impl, true, cst, (if keep then Some ty else None)
     | SectionLocalDef (c,t,opaq) -> 
         let cst = Global.push_named_def (id,c,t) in
-        let (_,bd,ty) = Global.lookup_named id in
-        CheckedSectionLocalDef (Option.get bd,ty,cst,opaq), false, None in
+        false, opaq, cst, None in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl keep;
   Dischargedhypsmap.set_discharged_hyps sp [];
-  vartab := Idmap.add id (p,vd,mk) !vartab
-
-let get_variable_constraints id = 
-  match pi2 (Idmap.find id !vartab) with
-  | CheckedSectionLocalDef (c,ty,cst,opaq) -> cst
-  | CheckedSectionLocalAssum (ty,cst) -> cst
+  add_variable_data id (p,opaq,cst,mk)
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) -> Some (Inl (get_variable_constraints id))
+  | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let (in_variable, out_variable) =
+let (inVariable, outVariable) =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -115,25 +78,17 @@ let (in_variable, out_variable) =
 
 (* for initial declaration *)
 let declare_variable id obj =
-  let oname = add_leaf id (in_variable (Inr (id,obj))) in
+  let oname = add_leaf id (inVariable (Inr (id,obj))) in
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope (VarRef id);
+  Heads.declare_head (EvalVarRef id);
   !xml_declare_variable oname;
   oname
 
-(* Globals: constants and parameters *)
+(** Declaration of constants and parameters *)
 
 type constant_declaration = constant_entry * logical_kind
 
-let csttab = ref (Spmap.empty : logical_kind Spmap.t)
-
-let _ = Summary.declare_summary "CONSTANT"
-	  { Summary.freeze_function = (fun () -> !csttab);
-	    Summary.unfreeze_function = (fun ft -> csttab := ft);
-	    Summary.init_function = (fun () -> csttab := Spmap.empty);
-	    Summary.survive_module = false;
-	    Summary.survive_section = false }
-
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
 let load_constant i ((sp,kn),(_,_,kind)) =
@@ -141,7 +96,7 @@ let load_constant i ((sp,kn),(_,_,kind)) =
     errorlabstrm "cache_constant" 
       (pr_id (basename sp) ++ str " already exists");
   Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn));
-  csttab := Spmap.add sp kind !csttab
+  add_constant_kind (constant_of_kn kn) kind
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
@@ -150,18 +105,14 @@ let open_constant i ((sp,kn),_) =
 let cache_constant ((sp,kn),(cdt,dhyps,kind)) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  if Idmap.mem id !vartab or Nametab.exists_cci sp then
+  if variable_exists id or Nametab.exists_cci sp then
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists");
   let kn' = Global.add_constant dir id cdt in
   assert (kn' = constant_of_kn kn);
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   add_section_constant kn' (Global.lookup_constant kn').const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  csttab := Spmap.add sp kind !csttab
-
-(*s Registration as global tables and rollback. *)
-
-open Cooking
+  add_constant_kind (constant_of_kn kn) kind
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
@@ -185,7 +136,7 @@ let export_constant cst = Some (dummy_constant cst)
 
 let classify_constant (_,cst) = Substitute (dummy_constant cst)
 
-let (in_constant, out_constant) =
+let (inConstant, outConstant) =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -206,9 +157,10 @@ let hcons_constant_declaration = function
   | cd -> cd
 
 let declare_constant_common id dhyps (cd,kind) =
-  let (sp,kn) = add_leaf id (in_constant (cd,dhyps,kind)) in
+  let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in
   let kn = constant_of_kn kn in
   declare_constant_implicits kn;
+  Heads.declare_head (EvalConstRef kn);
   Notation.declare_ref_arguments_scope (ConstRef kn);
   kn
 
@@ -221,7 +173,7 @@ let declare_constant_gen internal id (cd,kind) =
 let declare_internal_constant = declare_constant_gen true
 let declare_constant = declare_constant_gen false
 
-(* Inductives. *)
+(** Declaration of inductive blocks *)
 
 let declare_inductive_argument_scopes kn mie =
   list_iter_i (fun i {mind_entry_consnames=lc} ->
@@ -251,7 +203,7 @@ let inductive_names sp kn mie =
   in names
 
 let check_exists_inductive (sp,_) =
-  (if Idmap.mem (basename sp) !vartab then
+  (if variable_exists (basename sp) then
     errorlabstrm ""
       (pr_id (basename sp) ++ str " already exists"));
   if Nametab.exists_cci sp then
@@ -301,7 +253,7 @@ let dummy_inductive_entry (_,m) = ([],{
 
 let export_inductive x = Some (dummy_inductive_entry x)
 
-let (in_inductive, out_inductive) =
+let (inInductive, outInductive) =
   declare_object {(default_object "INDUCTIVE") with 
     cache_function = cache_inductive;
     load_function = load_inductive;
@@ -316,84 +268,9 @@ let declare_mind isrecord mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
     | [] -> anomaly "cannot declare an empty list of inductives" in
-  let (sp,kn as oname) = add_leaf id (in_inductive ([],mie)) in
+  let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in
   declare_mib_implicits kn;
   declare_inductive_argument_scopes kn mie;
   !xml_declare_inductive (isrecord,oname);
   oname
 
-(*s Test and access functions. *)
-
-let is_constant sp = 
-  try let _ = Spmap.find sp !csttab in true with Not_found -> false
-
-let constant_strength sp = Global
-let constant_kind sp = Spmap.find sp !csttab
-
-let get_variable id = 
-  let (p,x,_) = Idmap.find id !vartab in
-  match x with
-    | CheckedSectionLocalDef (c,ty,cst,opaq) -> (id,Some c,ty)
-    | CheckedSectionLocalAssum (ty,cst) -> (id,None,ty)
-
-let variable_strength _ = Local
-
-let find_section_variable id =
-  let (p,_,_) = Idmap.find id !vartab in Libnames.make_path p id
-
-let variable_opacity id =
-  let (_,x,_) = Idmap.find id !vartab in
-  match x with
-    | CheckedSectionLocalDef (c,ty,cst,opaq) -> opaq
-    | CheckedSectionLocalAssum (ty,cst) -> false (* any.. *)
-
-let variable_kind id =
-  pi3 (Idmap.find id !vartab)
-
-let clear_proofs sign =
-  List.fold_right
-    (fun (id,c,t as d) signv -> 
-      let d = if variable_opacity id then (id,None,t) else d in
-      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
-
-(* Global references. *)
-
-let first f v =
-  let n = Array.length v in
-  let rec look_for i =
-    if i = n then raise Not_found;
-    try f i v.(i) with Not_found -> look_for (succ i)
-  in
-  look_for 0
-
-let mind_oper_of_id sp id mib =
-  first
-    (fun tyi mip ->
-       if id = mip.mind_typename then 
-	 IndRef (sp,tyi)
-       else
-	 first 
-	   (fun cj cid -> 
-	      if id = cid then 
-		ConstructRef ((sp,tyi),succ cj) 
-	      else raise Not_found) 
-	   mip.mind_consnames)
-    mib.mind_packets
-
-let last_section_hyps dir =
-  fold_named_context
-    (fun (id,_,_) sec_ids ->
-      try
-        let (p,_,_) = Idmap.find id !vartab in
-        if dir=p then id::sec_ids else sec_ids
-      with Not_found -> sec_ids)
-    (Environ.named_context (Global.env()))
-    ~init:[]
-
-let is_section_variable = function
-  | VarRef _ -> true
-  | _ -> false
-
-let strength_of_global = function
-  | VarRef _ -> Local
-  | IndRef _ | ConstructRef _ | ConstRef _ -> Global
diff --git a/library/declare.mli b/library/declare.mli
index 96fd5eb9b..93c8b9f91 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -59,26 +59,6 @@ val declare_internal_constant :
    the whole block (boolean must be true iff it is a record) *)
 val declare_mind : bool -> mutual_inductive_entry -> object_name
 
-val strength_min : strength * strength -> strength
-val string_of_strength : strength -> string
-
-(*s Corresponding test and access functions. *)
-
-val is_constant : section_path -> bool
-val constant_strength : section_path -> strength
-val constant_kind : section_path -> logical_kind
-
-val get_variable : variable -> named_declaration
-val variable_strength : variable -> strength 
-val variable_kind : variable -> logical_kind
-val find_section_variable : variable -> section_path
-val last_section_hyps : dir_path -> identifier list
-val clear_proofs : named_context -> Environ.named_context_val
-
-(*s Global references *)
-
-val strength_of_global : global_reference -> strength
-
 (* hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (bool * constant -> unit) -> unit
diff --git a/library/decls.ml b/library/decls.ml
new file mode 100644
index 000000000..d84703271
--- /dev/null
+++ b/library/decls.ml
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(** This module registers tables for some non-logical informations
+     associated declarations *)
+
+open Names
+open Term
+open Sign
+open Decl_kinds
+open Libnames
+
+(** Datas associated to section variables and local definitions *)
+
+type variable_data =
+    dir_path * bool (* opacity *) * Univ.constraints * logical_kind
+
+let vartab = ref (Idmap.empty : variable_data Idmap.t)
+
+let _ = Summary.declare_summary "VARIABLE"
+  { Summary.freeze_function = (fun () -> !vartab);
+    Summary.unfreeze_function = (fun ft -> vartab := ft);
+    Summary.init_function = (fun () -> vartab := Idmap.empty);
+    Summary.survive_module = false;
+    Summary.survive_section = false }
+
+let add_variable_data id o = vartab := Idmap.add id o !vartab
+
+let variable_path id = let (p,_,_,_) = Idmap.find id !vartab in p
+let variable_opacity id = let (_,opaq,_,_) = Idmap.find id !vartab in opaq
+let variable_kind id = let (_,_,_,k) = Idmap.find id !vartab in k
+let variable_constraints id = let (_,_,cst,_) = Idmap.find id !vartab in cst
+
+let variable_exists id = Idmap.mem id !vartab
+
+(** Datas associated to global parameters and constants *)
+
+let csttab = ref (Cmap.empty : logical_kind Cmap.t)
+
+let _ = Summary.declare_summary "CONSTANT"
+	  { Summary.freeze_function = (fun () -> !csttab);
+	    Summary.unfreeze_function = (fun ft -> csttab := ft);
+	    Summary.init_function = (fun () -> csttab := Cmap.empty);
+	    Summary.survive_module = false;
+	    Summary.survive_section = false }
+
+let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
+
+let constant_kind kn = Cmap.find kn !csttab
+
+(** Miscellaneous functions. *)
+
+let clear_proofs sign =
+  List.fold_right
+    (fun (id,c,t as d) signv -> 
+      let d = if variable_opacity id then (id,None,t) else d in
+      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
+
+let last_section_hyps dir =
+  fold_named_context
+    (fun (id,_,_) sec_ids ->
+      try if dir=variable_path id then id::sec_ids else sec_ids
+      with Not_found -> sec_ids)
+    (Environ.named_context (Global.env()))
+    ~init:[]
+
+let is_section_variable = function
+  | VarRef _ -> true
+  | _ -> false
diff --git a/library/decls.mli b/library/decls.mli
new file mode 100644
index 000000000..96654bcbd
--- /dev/null
+++ b/library/decls.mli
@@ -0,0 +1,47 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: declare.mli 10741 2008-04-02 15:47:07Z msozeau $ i*)
+
+open Names
+open Sign
+(*
+open Libnames
+open Term
+open Declarations
+open Entries
+open Indtypes
+open Safe_typing
+open Nametab
+*)
+open Decl_kinds
+
+(** This module manages non-kernel informations about declarations. It
+    is either non-logical informations or logical informations that
+    have no place to be (yet) in the kernel *)
+
+(** Registration and access to the table of variable *)
+
+type variable_data = 
+    dir_path * bool (* opacity *) * Univ.constraints * logical_kind
+
+val add_variable_data : variable -> variable_data -> unit
+val variable_kind : variable -> logical_kind
+val variable_opacity : variable -> bool
+val variable_constraints : variable -> Univ.constraints
+val variable_exists : variable -> bool
+
+(** Registration and access to the table of constants *)
+
+val add_constant_kind : constant -> logical_kind -> unit
+val constant_kind : constant -> logical_kind
+
+(** Miscellaneous functions *)
+
+val last_section_hyps : dir_path -> identifier list
+val clear_proofs : named_context -> Environ.named_context_val
diff --git a/library/heads.ml b/library/heads.ml
new file mode 100644
index 000000000..c341c835e
--- /dev/null
+++ b/library/heads.ml
@@ -0,0 +1,190 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Pp
+open Util
+open Names
+open Term
+open Mod_subst
+open Environ
+open Libnames
+open Nameops
+open Libobject
+open Lib
+
+(** Characterization of the head of a term *)
+
+(* We only compute an approximation to ensure the computation is not
+   arbitrary long (e.g. the head constant of [h] defined to be 
+   [g (fun x -> phi(x))] where [g] is [fun f => g O] does not launch 
+   the evaluation of [phi(0)] and the head of [h] is declared unknown). *)
+
+type rigid_head_kind =
+| RigidParameter of constant (* a Const without body *)
+| RigidVar of variable (* a Var without body *)
+| RigidType (* an inductive, a product or a sort *)
+
+type head_approximation =
+| RigidHead of rigid_head_kind
+| ConstructorHead
+| FlexibleHead of int * int * int * bool (* [true] if a surrounding case *)
+| NotImmediatelyComputableHead
+
+(** Registration as global tables and rollback. *)
+
+module Evalreford = struct
+  type t = evaluable_global_reference
+  let compare = Pervasives.compare
+end
+
+module Evalrefmap = Map.Make(Evalreford)
+
+let head_map = ref Evalrefmap.empty
+
+let init () = head_map := Evalrefmap.empty
+
+let freeze () = !head_map
+
+let unfreeze hm = head_map := hm
+
+let _ = 
+  Summary.declare_summary "Head_decl"
+    { Summary.freeze_function = freeze;
+      Summary.unfreeze_function = unfreeze;
+      Summary.init_function = init;
+      Summary.survive_module = true;
+      Summary.survive_section = false }
+
+let variable_head id  = Evalrefmap.find (EvalVarRef id) !head_map
+let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map
+
+let kind_of_head env t =
+  let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with
+  | Rel n when n > k -> NotImmediatelyComputableHead
+  | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
+  | Var id -> 
+      (try on_subterm k l b (variable_head id)
+       with Not_found ->
+        (* a goal variable *)
+        match pi2 (lookup_named id env) with
+        | Some c -> aux k l c b
+        | None -> NotImmediatelyComputableHead)
+  | Const cst -> on_subterm k l b (constant_head cst)
+  | Construct _ | CoFix _ -> 
+      if b then NotImmediatelyComputableHead else ConstructorHead
+  | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
+  | Cast (c,_,_) -> aux k l c b
+  | Lambda (_,_,c) when l = [] -> assert (not b); aux (k+1) [] c b
+  | Lambda (_,_,c) -> aux (k+1) (List.tl l) (subst1 (List.hd l) c) b
+  | LetIn _ -> assert false
+  | Meta _ | Evar _ -> NotImmediatelyComputableHead
+  | App (c,al) -> aux k (Array.to_list al @ l) c b
+  | Case (_,_,c,_) -> aux k [] c true
+  | Fix ((i,j),_) ->
+      let n = i.(j) in
+      try aux k [] (List.nth l n) true
+      with Failure _ -> FlexibleHead (k + n + 1, k + n + 1, 0, true)
+  and on_subterm k l with_case = function
+  | FlexibleHead (n,i,q,with_subcase) ->
+      let m = List.length l in
+      let k',rest,a = 
+        if n > m then
+          (* eta-expansion *)
+          let a =
+            if i <= m then
+              (* we pick the head in the existing arguments *)
+              lift (n-m) (List.nth l (i-1))
+            else
+              (* we pick the head in the added arguments *)
+              mkRel (n-i+1) in
+          k+n-m,[],a
+        else
+          (* enough arguments to [cst] *)
+          k,list_skipn n l,List.nth l (i-1) in
+      let l' = list_tabulate (fun _ -> mkMeta 0) q @ rest in
+      aux k' l' a (with_subcase or with_case)
+  | ConstructorHead when with_case -> NotImmediatelyComputableHead
+  | x -> x
+  in aux 0 [] t false
+
+let compute_head = function
+| EvalConstRef cst ->
+    (match constant_opt_value (Global.env()) cst with
+     | None -> RigidHead (RigidParameter cst)
+     | Some c -> kind_of_head (Global.env()) c)
+| EvalVarRef id ->
+    (match pi2 (Global.lookup_named id) with
+     | Some c when not (Decls.variable_opacity id) -> 
+           kind_of_head (Global.env()) c
+     | _ -> 
+           RigidHead (RigidVar id))
+
+let is_rigid env t = 
+  match kind_of_head env t with
+  | RigidHead _ | ConstructorHead -> true
+  | _ -> false
+
+(** Registration of heads as an object *)
+
+let load_head _ (_,(ref,(k:head_approximation))) =
+  head_map := Evalrefmap.add ref k !head_map
+  
+let cache_head o =
+  load_head 1 o
+
+let subst_head_approximation subst = function
+  | RigidHead (RigidParameter cst) as k ->
+      let cst,c = subst_con subst cst in
+      if c = mkConst cst then
+        (* A change of the prefix of the constant *)
+        k
+      else
+        (* A substitution of the constant by a functor argument *)
+        kind_of_head (Global.env()) c
+  | x -> x
+
+let subst_head (_,subst,(ref,k)) =
+  (subst_evaluable_reference subst ref, subst_head_approximation subst k)
+
+let discharge_head (_,(ref,k)) =
+  match ref with
+  | EvalConstRef cst -> Some (EvalConstRef (pop_con cst), k)
+  | EvalVarRef id -> None
+
+let rebuild_head (info,(ref,k)) =
+  (ref, compute_head ref)
+
+let export_head o = Some o
+
+let (inHead, _) =
+  declare_object {(default_object "HEAD") with 
+    cache_function = cache_head;
+    load_function = load_head;
+    subst_function = subst_head;
+    classify_function = (fun (_,x) -> Substitute x);
+    discharge_function = discharge_head;
+    rebuild_function = rebuild_head;
+    export_function = export_head }
+
+let declare_head c =
+  let hd = compute_head c in
+  add_anonymous_leaf (inHead (c,hd))
+
+(** Printing *)
+
+let pr_head = function
+| RigidHead (RigidParameter cst) -> str "rigid constant " ++ pr_con cst
+| RigidHead (RigidType) -> str "rigid type"
+| RigidHead (RigidVar id) -> str "rigid variable " ++ pr_id id
+| ConstructorHead -> str "constructor"
+| FlexibleHead (k,n,p,b) -> int n ++ str "th of " ++ int k ++ str " binders applied to " ++ int p ++ str " arguments" ++ (if b then str " (with case)" else mt())
+| NotImmediatelyComputableHead -> str "unknown"
+
+
diff --git a/library/heads.mli b/library/heads.mli
new file mode 100644
index 000000000..4a086b9dc
--- /dev/null
+++ b/library/heads.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Names
+open Term
+open Environ
+
+(** This module is about the computation of an approximation of the
+    head symbol of defined constants and local definitions; it
+    provides the function to compute the head symbols and a table to
+    store the heads *)
+
+(* [declared_head] computes and registers the head symbol of a
+   possibly evaluable constant or variable *)
+
+val declare_head : evaluable_global_reference -> unit
+
+(* [is_rigid] tells if some term is known to ultimately reduce to a term
+    with a rigid head symbol *)
+
+val is_rigid : env -> constr -> bool
diff --git a/library/libobject.mli b/library/libobject.mli
index 15de388ea..33ad67c84 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -51,6 +51,14 @@ open Mod_subst
      this function should be declared for substitutive objects 
      only (see obove)
 
+   * a discharge function, that is applied at section closing time to
+     collect the data necessary to rebuild the discharged form of the
+     non volatile objects
+
+   * a rebuild function, that is applied after section closing to
+     rebuild the non volatile content of a section from the data
+     collected by the discharge function
+
    * an export function, to enable optional writing of its contents 
      to disk (.vo). This function is also the oportunity to remove 
      redundant information in order to keep .vo size small