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

46 files changed, 684 insertions, 370 deletions

diff --git a/Makefile.common b/Makefile.common
index edc9ad9e4..cf0f234d7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -140,7 +140,8 @@ LIBRARY:=\
   library/nameops.cmo library/libnames.cmo library/libobject.cmo \
   library/summary.cmo library/nametab.cmo library/global.cmo library/lib.cmo \
   library/declaremods.cmo library/library.cmo library/states.cmo \
-  library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo
+  library/decl_kinds.cmo library/dischargedhypsmap.cmo library/goptions.cmo \
+  library/decls.cmo library/heads.cmo
 
 PRETYPING:=\
   pretyping/termops.cmo pretyping/evd.cmo \
@@ -456,7 +457,7 @@ PRINTERSCMO:=\
   kernel/term_typing.cmo kernel/mod_typing.cmo kernel/safe_typing.cmo	\
   library/summary.cmo library/global.cmo library/nameops.cmo		\
   library/libnames.cmo library/nametab.cmo library/libobject.cmo	\
-  library/lib.cmo library/goptions.cmo \
+  library/lib.cmo library/goptions.cmo library/decls.cmo library/heads.cmo \
   pretyping/termops.cmo pretyping/evd.cmo pretyping/rawterm.cmo \
   pretyping/reductionops.cmo pretyping/inductiveops.cmo			    \
   pretyping/retyping.cmo pretyping/cbv.cmo				    \
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index b82526200..a4dc0eacd 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -408,7 +408,7 @@ let inspect n =
              	oname, Lib.Leaf lobj ->
 		  (match oname, object_tag lobj with
                        (sp,_), "VARIABLE" ->
-			 let (_, _, v) = get_variable (basename sp) in
+			 let (_, _, v) = Global.lookup_named (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | (sp,kn), "CONSTANT" ->
 			 let typ = Typeops.type_of_constant (Global.env()) (constant_of_kn kn) in
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 172c7479c..6b17e7396 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -158,7 +158,7 @@ let constant_to_ast_list kn =
 	make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
 
 let variable_to_ast_list sp =
-  let (id, c, v) = get_variable sp in
+  let (id, c, v) = Global.lookup_named sp in
   let l = implicits_of_global (VarRef sp) in
     (match c with
 	 None -> 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index afe7fc6d2..7d4eb72a9 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -27,6 +27,7 @@ open Typing
 open Tacmach
 open Tactics
 open Nametab
+open Decls
 open Declare
 open Decl_kinds
 open Tacred
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 0f9331ff5..9eac4fbae 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -523,6 +523,9 @@ module Coercion = struct
       | Some (init, cur) ->
 	  (isevars, cj)
 
+  let inh_conv_coerce_rigid_to _ _ _ _ _ =
+    failwith "inh_conv_coerce_rigid_to: TODO"
+
   let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) =
 (*     (try *)
 (*        trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++ *)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 3551b262c..1bd5bb970 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -89,11 +89,11 @@ val string_of_hole_kind : hole_kind -> string
 val evars_of_term : evar_map -> evar_map -> constr -> evar_map
 val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map
 val global_kind : logical_kind
-val goal_kind : locality_flag * goal_object_kind
+val goal_kind : locality * goal_object_kind
 val global_proof_kind : logical_kind
-val goal_proof_kind : locality_flag * goal_object_kind
+val goal_proof_kind : locality * goal_object_kind
 val global_fix_kind : logical_kind
-val goal_fix_kind : locality_flag * goal_object_kind
+val goal_fix_kind : locality * goal_object_kind
 
 val mkSubset : name -> constr -> constr -> constr
 val mkProj1 : constr -> constr -> constr -> constr
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 5515320f0..6ea000f5b 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -55,7 +55,7 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
 
 
 let get_uri_of_var v pvars =
- let module D = Declare in
+ let module D = Decls in
  let module N = Names in
   let rec search_in_open_sections =
    function
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 649139f35..7e3a1bd41 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -73,11 +73,7 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
   let tag = Libobject.object_tag o in
    print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
-      "CONSTANT" ->
-        (match D.constant_strength sp with
-          | DK.Local  -> false (* a local definition *)
-          | DK.Global -> true  (* a non-local one    *)
-        )
+      "CONSTANT"        -> true   (* constants/parameters are non global *)
     | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
     | "VARIABLE"        -> false  (* variables are local, so no namesakes     *)
     | _                 -> false  (* uninteresting thing that won't be printed*)
@@ -154,7 +150,7 @@ let search_variables () =
      | he::tl as modules ->
         let one_section_variables =
          let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
-          let t = List.map N.string_of_id (Declare.last_section_hyps dirpath) in
+          let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in
            [he,t]
         in
          one_section_variables @ aux tl
@@ -443,7 +439,7 @@ let kind_of_inductive isrecord kn =
 
 let kind_of_variable id =
   let module DK = Decl_kinds in
-  match Declare.variable_kind id with
+  match Decls.variable_kind id with
     | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
     | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
     | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
@@ -454,7 +450,7 @@ let kind_of_variable id =
 
 let kind_of_constant kn = 
   let module DK = Decl_kinds in
-  match Declare.constant_kind (Nametab.sp_of_global(Libnames.ConstRef kn)) with
+  match Decls.constant_kind kn with
     | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
     | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
     | DK.IsAssumption DK.Conjectural ->
@@ -540,11 +536,10 @@ let print internal glob_ref kind xml_library_root =
   let tag,obj =
    match glob_ref with
       Ln.VarRef id ->
-       let sp = Declare.find_section_variable id in
        (* this kn is fake since it is not provided by Coq *)
        let kn = 
         let (mod_path,dir_path) = Lib.current_prefix () in
-        N.make_kn mod_path dir_path (N.label_of_id (Ln.basename sp))
+        N.make_kn mod_path dir_path (N.label_of_id id)
        in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
diff --git a/dev/base_include b/dev/base_include
index 83e23d29f..d3301c88b 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -72,6 +72,7 @@ open Classops
 open Clenv
 open Rawterm
 open Coercion
+open Coercion.Default
 open Recordops
 open Detyping
 open Reductionops
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index dfd813985..c67307d36 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -48,6 +48,7 @@ let ppcon con = pp(pr_con con)
 let ppkn kn = pp(pr_kn kn)
 let ppsp sp = pp(pr_sp sp)
 let ppqualid qid = pp(pr_qualid qid)
+let ppclindex cl = pp(Classops.pr_cl_index cl)
 
 (* term printers *)
 let rawdebug = ref false
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index f60e2dbe0..ac4efc515 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -653,7 +653,7 @@ let check_one_fix renv recpos def =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
-      let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
+      let (f,l) = decompose_app (whd_betaiotazeta t) in
       match kind_of_term f with
         | Rel p -> 
             (* Test if [p] is a fixpoint (recursive call) *) 
diff --git a/kernel/names.ml b/kernel/names.ml
index 38eb38bea..d1c6ee8a4 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -65,7 +65,7 @@ let repr_dirpath x = x
 let empty_dirpath = []
 
 let string_of_dirpath = function
-  | [] -> "_empty_"
+  | [] -> "<>"
   | sl -> String.concat "." (List.map string_of_id (List.rev sl))
 
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 7a6c560f8..ba7e8c41d 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -90,11 +90,11 @@ let pure_stack lfts stk =
 let nf_betaiota t =
   norm_val (create_clos_infos betaiota empty_env) (inject t)
 
-let whd_betaiotazeta env x =
+let whd_betaiotazeta x =
   match kind_of_term x with
     | (Sort _|Var _|Meta _|Evar _|Const _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> x
-    | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x)
+    | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
 
 let whd_betadeltaiota env t = 
   match kind_of_term t with
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 663c18e2c..2e344b217 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -17,7 +17,7 @@ open Closure
 (************************************************************************)
 (*s Reduction functions *)
 
-val whd_betaiotazeta        : env -> constr -> constr
+val whd_betaiotazeta        : constr -> constr
 val whd_betadeltaiota       : env -> constr -> constr
 val whd_betadeltaiota_nolet : env -> constr -> constr
 
diff --git a/lib/gset.mli b/lib/gset.mli
index af8764a9c..78fc61e14 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -26,7 +26,7 @@ val compare : 'a t -> 'a t -> int
 val equal : 'a t -> 'a t -> bool
 val subset : 'a t -> 'a t -> bool
 val iter : ('a -> unit) -> 'a t -> unit
-val fold : ('a -> 'a -> 'a) -> 'a t -> 'a -> 'a
+val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
 val cardinal : 'a t -> int
 val elements : 'a t -> 'a list
 val min_elt : 'a t -> 'a
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 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 48fe40cab..6ca3a5c1a 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -360,12 +360,12 @@ let gallina_print_inductive sp =
     (print_inductive_implicit_args sp mipv ++
      print_inductive_argument_scopes sp mipv)
 
-let print_named_decl sp = 
-  gallina_print_named_decl (get_variable sp) ++ fnl ()
+let print_named_decl id = 
+  gallina_print_named_decl (Global.lookup_named id) ++ fnl ()
 
-let gallina_print_section_variable sp =
-  print_named_decl sp ++
-  with_line_skip (print_name_infos (VarRef sp))
+let gallina_print_section_variable id =
+  print_named_decl id ++
+  with_line_skip (print_name_infos (VarRef id))
 
 let print_body = function
   | Some lc  -> pr_lconstr (Declarations.force lc)
diff --git a/parsing/search.ml b/parsing/search.ml
index fd9eb12bb..88b51907b 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -50,11 +50,11 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
   let crible_rec (sp,_) lobj = match object_tag lobj with
     | "VARIABLE" ->
 	(try 
-	   let (idc,_,typ) = get_variable (basename sp) in 
+	   let (id,_,typ) = Global.lookup_named (basename sp) in 
            if refopt = None
 	     || head_const typ = constr_of_global (Option.get refopt)
 	   then
-	     fn (VarRef idc) env typ
+	     fn (VarRef id) env typ
 	 with Not_found -> (* we are in a section *) ())
     | "CONSTANT" ->
 	let cst = locate_constant (qualid_of_sp sp) in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5b0c2eb36..0d7e3d611 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -44,7 +44,7 @@ type coe_typ = global_reference
 type coe_info_typ = {
   coe_value : constr;
   coe_type : types;
-  coe_strength : strength;
+  coe_strength : locality;
   coe_is_identity : bool;
   coe_param : int }
 
@@ -290,7 +290,7 @@ let add_coercion_in_graph (ic,source,target) =
   if (!ambig_paths <> []) && is_verbose () then 
     ppnl (message_ambig !ambig_paths)
 
-type coercion = coe_typ * strength * bool * cl_typ * cl_typ * int
+type coercion = coe_typ * locality * bool * cl_typ * cl_typ * int
 
 (* Calcul de l'arité d'une classe *)
 
@@ -304,7 +304,7 @@ let class_params = function
   | CL_SECVAR sp -> reference_arity_length (VarRef sp)
   | CL_IND sp  -> reference_arity_length (IndRef sp)
 
-(* add_class : cl_typ -> strength option -> bool -> unit *)
+(* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
 let add_class cl =
   add_new_class cl { cl_param = class_params cl }
@@ -366,6 +366,8 @@ let coercion_identity v = v.coe_is_identity
 (* For printing purpose *)
 let get_coercion_value v = v.coe_value
 
+let pr_cl_index n = int n
+
 let classes () = Bijint.dom !class_tab
 let coercions () = Gmap.rng !coercion_tab
 let inheritance_graph () = Gmap.to_list !inheritance_graph
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index dd51ee970..c1a62b34f 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -66,7 +66,7 @@ val class_args_of : constr -> constr list
 
 (*s [declare_coercion] adds a coercion in the graph of coercion paths *)
 val declare_coercion : 
-  coe_typ -> strength -> isid:bool ->
+  coe_typ -> locality -> isid:bool ->
       src:cl_typ -> target:cl_typ -> params:int -> unit
 
 (*s Access to coercions infos *)
@@ -90,6 +90,7 @@ val install_path_printer :
 (*s This is for printing purpose *)
 val string_of_class : cl_typ -> string
 val pr_class : cl_typ -> std_ppcmds
+val pr_cl_index : cl_index -> std_ppcmds
 val get_coercion_value : coe_index -> constr
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
 val classes : unit -> cl_typ list
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index ed9d779ad..e7423c748 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -28,15 +28,7 @@ open Unification
 open Mod_subst
 open Coercion.Default
 
-(* *)
-let w_coerce env c ctyp target evd =
-  try
-    let j = make_judge c ctyp in
-    let tycon = mk_tycon_type target in
-    let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in
-    (evd',j'.uj_val)
-  with e when precatchable_exception e ->
-    evd,c
+(* Abbreviations *)
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
 let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
@@ -398,36 +390,24 @@ let error_already_defined b =
         anomalylabstrm ""
           (str "Position " ++ int n ++ str" already defined")
 
-let rec similar_type_shapes t u =
-  let t,_ = decompose_app t and u,_ = decompose_app u in
-  match kind_of_term t, kind_of_term u with
-  | Prod (_,t1,t2), Prod (_,u1,u2) -> similar_type_shapes t2 u2
-  | Const cst, Const cst' -> cst = cst'
-  | Var id, Var id' -> id = id'
-  | Ind ind, Ind ind' -> ind = ind'
-  | Rel n, Rel n' -> n = n'
-  | Sort s, Sort s' -> family_of_sort s = family_of_sort s'
-  | Case (_,_,c,_), Case (_,_,c',_) -> similar_type_shapes c c'
-  | _ -> false
-
-let clenv_unify_similar_types clenv c t u =
-  if occur_meta u then
-    if similar_type_shapes t u then
-      try TypeProcessed, clenv_unify true CUMUL t u clenv, c
-      with e when precatchable_exception e -> TypeNotProcessed, clenv, c
-    else
-      CoerceToType, clenv, c
+let clenv_unify_binding_type clenv c t u =
+  if isMeta (fst (whd_stack u)) then
+    (* Not enough information to know if some subtyping is needed *)
+    CoerceToType, clenv, c
   else
-    let evd,c = w_coerce (cl_env clenv) c t u clenv.evd in
-    TypeProcessed, { clenv with evd = evd }, c
+    (* Enough information so as to try a coercion now *)
+    try
+      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
+      TypeProcessed, { clenv with evd = evd }, c
+    with e when precatchable_exception e ->
+      TypeNotProcessed, clenv, c
 
 let clenv_assign_binding clenv k (sigma,c) =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
   let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
   let c_typ = clenv_hnf_constr clenv' c_typ in
-  let status,clenv'',c = clenv_unify_similar_types clenv' c c_typ k_typ in
-(*  let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in*)
+  let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
   { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
 
 let clenv_match_args bl clenv =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 729bd84f1..bd023721a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -48,7 +48,9 @@ module type S = sig
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
     env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
-    
+
+  val inh_conv_coerce_rigid_to : loc -> 
+    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
 
   (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
@@ -158,7 +160,11 @@ module Default = struct
 
   let inh_coerce_to_base loc env evd j = (evd, j)
 
-  let inh_coerce_to_fail env evd c1 v t =
+  let inh_coerce_to_fail env evd rigidonly v c1 t =
+    if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
+    then
+      raise NoCoercion
+    else
     let v', t' =
       try 
 	let t1,i1 = class_of1 env evd c1 in
@@ -171,77 +177,44 @@ module Default = struct
 	    | None -> None, t
       with Not_found -> raise NoCoercion 
     in
-      try (the_conv_x_leq env t' c1 evd, v', t')
+      try (the_conv_x_leq env t' c1 evd, v')
       with Reduction.NotConvertible -> raise NoCoercion
 
-  let rec inh_conv_coerce_to_fail loc env evd v t c1 =
-    try (the_conv_x_leq env t c1 evd, v, t)
+  let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
+    try (the_conv_x_leq env t c1 evd, v)
     with Reduction.NotConvertible ->
-    try inh_coerce_to_fail env evd c1 v t
+    try inh_coerce_to_fail env evd rigidonly v c1 t
     with NoCoercion ->
     match
       kind_of_term (whd_betadeltaiota env (evars_of evd) t),
       kind_of_term (whd_betadeltaiota env (evars_of evd) c1)
     with
-    | Prod (_,t1,t2), Prod (name,u1,u2) -> 
-	let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in
-	let (evd',b) =
-	  match v' with 
-	  | Some v' ->
-	      (match kind_of_term v' with
-	       | Lambda (x,v1,v2) ->
-		   (* sous-typage non contravariant: pas de "leq v1 u1" *)
-		   (try the_conv_x env v1 u1 evd, Some (x, v1, v2)
-		   with Reduction.NotConvertible -> (evd, None))
-	       | _  -> (evd, None))
-	  | None -> (evd, None)
-	in
-	(match b with
-	 | Some (x, v1, v2) ->
-	     let env1 = push_rel (x,None,v1) env in
-	     let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd'
-	       (Some v2) t2 u2 in
-	     (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', 
-	     mkProd (x, v1, t2'))
-	 | None ->
-	     (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-	     (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-	     (* has type (name:u1)u2 (with v' recursively obtained) *)
-	     let name = match name with 
-	       | Anonymous -> Name (id_of_string "x")
-	       | _ -> name
-	     in
-	     let env1 = push_rel (name,None,u1) env in
-	     let (evd', v1', t1') =
-	       inh_conv_coerce_to_fail loc env1 evd
-		 (Some (mkRel 1)) (lift 1 u1) (lift 1 t1)
-	     in
-	     let (evd'', v2', t2') = 
-	       let v2 =
-		 match v with 
-		 | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1'
-		 | None -> None
-	       and evd', t2 =
-		 match v1' with 
-		 | Some v1' -> evd', subst_term v1' t2
-		 | None -> 
-		     let evd', ev =
-		       new_evar evd' env ~src:(loc, InternalHole) t1' in
-		     evd', subst_term ev t2
-	       in
-	       inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
-	     in
-	     (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2',
-	     mkProd (name, u1, t2')))
+    | Prod (name,t1,t2), Prod (_,u1,u2) -> 
+        (* Conversion did not work, we may succeed with a coercion. *)
+        (* We eta-expand (hence possibly modifying the original term!) *)
+	(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
+	(* has type forall (x:u1), u2 (with v' recursively obtained) *)
+	let name = match name with 
+	  | Anonymous -> Name (id_of_string "x")
+	  | _ -> name in
+	let env1 = push_rel (name,None,u1) env in
+	let (evd', v1) =
+	  inh_conv_coerce_to_fail loc env1 evd rigidonly
+            (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
+        let v1 = Option.get v1 in
+	let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
+        let t2 = subst_term v1 t2 in
+	let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
+	(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
     | _ -> raise NoCoercion
 
   (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to loc env evd cj (n, t) =
+  let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) =
     match n with
 	None ->
-	  let (evd', val', type') = 
+	  let (evd', val') = 
 	    try 
-	      inh_conv_coerce_to_fail loc env evd (Some cj.uj_val) cj.uj_type t
+	      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
 	    with NoCoercion ->
 	      let sigma = evars_of evd in
 		error_actual_type_loc loc env sigma cj t
@@ -249,6 +222,10 @@ module Default = struct
 	  let val' = match val' with Some v -> v | None -> assert(false) in
 	    (evd',{ uj_val = val'; uj_type = t })
       | Some (init, cur) -> (evd, cj)
+
+  let inh_conv_coerce_to = inh_conv_coerce_to_gen false
+  let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
+
       
     let inh_conv_coerces_to loc env (evd : evar_defs) t (abs, t') = evd
       (* Still problematic, as it changes unification 
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 5476a4820..00735d874 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -45,6 +45,9 @@ module type S = sig
      [j.uj_type] are convertible; it fails if no coercion is applicable *)
   val inh_conv_coerce_to : loc -> 
     env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
+
+  val inh_conv_coerce_rigid_to : loc -> 
+    env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment
     
   (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
      is coercible to an object of type [t'] adding evar constraints if needed;
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 3adf749f0..ddc3654dc 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -341,7 +341,7 @@ let mk_freelisted c =
 
 let map_fl f cfl = { cfl with rebus=f cfl.rebus }
 
-(* Status of an instance wrt to the meta it solves:
+(* Status of an instance found by unification wrt to the meta it solves:
   - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
   - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
   - a term that can be eta-expanded n times while still being a solution
@@ -351,9 +351,24 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus }
 type instance_constraint =
     IsSuperType | IsSubType | ConvUpToEta of int | UserGiven
 
+(* Status of the unification of the type of an instance against the type of
+     the meta it instantiates:
+   - CoerceToType means that the unification of types has not been done
+     and that a coercion can still be inserted: the meta should not be
+     substituted freely (this happens for instance given via the
+     "with" binding clause).
+   - TypeProcessed means that the information obtainable from the
+     unification of types has been extracted.
+   - TypeNotProcessed means that the unification of types has not been
+     done but it is known that no coercion may be inserted: the meta
+     can be substituted freely.
+*)
+
 type instance_typing_status =
     CoerceToType | TypeNotProcessed | TypeProcessed
 
+(* Status of an instance together with the status of its type unification *)
+
 type instance_status = instance_constraint * instance_typing_status
 
 (* Clausal environments *)
@@ -519,6 +534,13 @@ let metas_of evd =
     | (n,Cltyp (_,typ))  -> (n,typ.rebus))
     (meta_list evd)
 
+let map_metas_fvalue f evd =
+  { evd with metas =
+      Metamap.map 
+        (function 
+          | Clval(id,(c,s),typ) -> Clval(id,(mk_freelisted (f c.rebus),s),typ)
+          | x -> x) evd.metas }
+
 let meta_opt_fvalue evd mv =
   match Metamap.find mv evd.metas with
     | Clval(_,b,_) -> Some b
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 352d3021d..71c6bb0dc 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -122,11 +122,28 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
 type instance_constraint = 
     IsSuperType | IsSubType | ConvUpToEta of int | UserGiven
 
+(* Status of the unification of the type of an instance against the type of
+     the meta it instantiates:
+   - CoerceToType means that the unification of types has not been done
+     and that a coercion can still be inserted: the meta should not be
+     substituted freely (this happens for instance given via the
+     "with" binding clause).
+   - TypeProcessed means that the information obtainable from the
+     unification of types has been extracted.
+   - TypeNotProcessed means that the unification of types has not been
+     done but it is known that no coercion may be inserted: the meta
+     can be substituted freely.
+*)
+
 type instance_typing_status =
     CoerceToType | TypeNotProcessed | TypeProcessed
 
+(* Status of an instance together with the status of its type unification *)
+
 type instance_status = instance_constraint * instance_typing_status
 
+(* Clausal environments *)
+
 type clbinding =
   | Cltyp of name * constr freelisted
   | Clval of name * (constr freelisted * instance_status) * constr freelisted
@@ -198,6 +215,7 @@ val meta_merge : evar_defs -> evar_defs -> evar_defs
 
 val undefined_metas : evar_defs -> metavariable list
 val metas_of : evar_defs -> metamap
+val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs
 
 type metabinding = metavariable * constr * instance_status
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index e118a659e..e825b3f48 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -946,7 +946,7 @@ let meta_reducible_instance evd b =
 	(match
 	  try
 	    let g,s = List.assoc m metas in
-	    if isConstruct g or s = TypeProcessed then Some g else None
+	    if isConstruct g or s <> CoerceToType then Some g else None
 	  with Not_found -> None
 	  with
 	    | Some g -> irec (mkCase (ci,p,g,bl))
@@ -956,13 +956,13 @@ let meta_reducible_instance evd b =
 	(match
 	  try
 	    let g,s = List.assoc m metas in
-	    if isLambda g or s = TypeProcessed then Some g else None
+	    if isLambda g or s <> CoerceToType then Some g else None
 	  with Not_found -> None
 	 with
 	   | Some g -> irec (mkApp (g,l))
 	   | None -> mkApp (f,Array.map irec l))
     | Meta m ->
-	(try let g,s = List.assoc m metas in if s=TypeProcessed then irec g else u
+	(try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u
 	 with Not_found -> u)
     | _ -> map_constr irec u
   in 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c5e9dff8b..b140ad51a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -24,6 +24,7 @@ open Pattern
 open Evarutil
 open Pretype_errors
 open Retyping
+open Coercion.Default
 
 (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
    gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
@@ -380,14 +381,39 @@ let is_mimick_head f =
       (Const _|Var _|Rel _|Construct _|Ind _) -> true
     | _ -> false
 
-let w_coerce env c ctyp target evd =
+let pose_all_metas_as_evars env evd t =
+  let evdref = ref evd in
+  let rec aux t = match kind_of_term t with
+  | Meta mv ->
+      (match Evd.meta_opt_fvalue !evdref mv with
+       | Some ({rebus=c},_) -> c
+       | None ->
+        let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
+        let ty = if mvs = Evd.Metaset.empty then ty else aux ty in
+        let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in
+        evdref := meta_assign mv (ev,(ConvUpToEta 0,TypeNotProcessed)) !evdref;
+        ev)
+  | _ ->
+      map_constr aux t in
+  let c = aux t in
+  (* side-effect *)
+  (!evdref, c)
+
+let w_coerce_to_type env evd c cty mvty =
   try
-    let j = make_judge c ctyp in
-    let tycon = mk_tycon_type target in
-    let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j tycon in
+    let j = make_judge c cty in
+    let evd,mvty = pose_all_metas_as_evars env evd mvty in
+    let tycon = mk_tycon_type mvty in
+    let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
+    let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
     (evd',j'.uj_val)
   with e when precatchable_exception e ->
-    evd,c
+    (evd,c)
+
+let w_coerce env evd mv c =
+  let cty = get_type_of env (evars_of evd) c in
+  let mvty = Typing.meta_type evd mv in
+  w_coerce_to_type env evd c cty mvty
 
 let unify_to_type env evd flags c u =
   let sigma = evars_of evd in
@@ -398,20 +424,6 @@ let unify_to_type env evd flags c u =
   try unify_0 env sigma Cumul flags t u
   with e when precatchable_exception e -> ([],[])
 
-let coerce_to_type env evd c u =
-  let c = refresh_universes c in
-  let t = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
-  w_coerce env c t u evd
-
-let unify_or_coerce_type env evd flags mv c =
-  let mvty = Typing.meta_type evd mv in
-  (* nf_betaiota was before in type_of - useful to reduce
-     types like (x:A)([x]P u) *)
-  if occur_meta mvty then
-    (evd,c),unify_to_type env evd flags c mvty
-  else
-    coerce_to_type env evd c mvty,([],[])
-
 let unify_type env evd flags mv c =
   let mvty = Typing.meta_type evd mv in
   if occur_meta mvty then
@@ -471,7 +483,7 @@ let w_merge env with_types flags metas evars evd =
 	  if with_types & to_type <> TypeProcessed then
 	    if to_type = CoerceToType then
               (* Some coercion may have to be inserted *)
-	      (unify_or_coerce_type env evd flags mv c,[])
+	      (w_coerce env evd mv c,([],[])),[]
 	    else
               (* No coercion needed: delay the unification of types *)
 	      ((evd,c),([],[])),(mv,c)::eqns
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 9156623f5..1b8f9ccd8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -35,6 +35,11 @@ val w_unify_to_subterm :
 
 val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs
 
+(* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type
+   [ctyp] so that its gets type [typ]; [typ] may contain metavariables *)
+val w_coerce_to_type : env -> evar_defs -> constr -> types -> types ->
+  evar_defs * constr
+
 (*i This should be in another module i*)
 
 (* [abstract_list_all env evd t c l]                       *)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index ca25c722c..a13f8bf70 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -16,6 +16,7 @@ open Rawterm
 open Util
 open Genarg
 open Pattern
+open Decl_kinds
 
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
@@ -325,4 +326,4 @@ type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 
 type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
-type declaration_hook = Decl_kinds.strength -> global_reference -> unit
+type declaration_hook = locality -> global_reference -> unit
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 5402e6120..e3e90c7ca 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -207,7 +207,7 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x
 
 
 (* Declaration of the Hint Rewrite library object *)
-let (in_hintrewrite,out_hintrewrite)=
+let (inHintRewrite,outHintRewrite)=
   Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with
        Libobject.cache_function = cache_hintrewrite;
        Libobject.load_function = (fun _ -> cache_hintrewrite);
@@ -223,4 +223,4 @@ let add_rew_rules base lrul =
       (c,mkProp (* dummy value *), b,Tacinterp.glob_tactic t)
     ) lrul
   in
-   Lib.add_anonymous_leaf (in_hintrewrite (base,lrul))
+   Lib.add_anonymous_leaf (inHintRewrite (base,lrul))
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index b19df1aee..dc8ff2b9c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -923,7 +923,7 @@ let new_morphism m signature id hook =
 	new_edited id
 	  (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr);
 	Pfedit.start_proof id (Global, Proof Lemma) 
-	  (Declare.clear_proofs (Global.named_context ()))
+	  (Decls.clear_proofs (Global.named_context ()))
 	  lem hook;
 	Flags.if_verbose msg (Printer.pr_open_subgoals ());
       end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 34c2f690c..d3f7cc5f1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -909,10 +909,12 @@ let specialize mopt (c,lbind) g =
     (match kind_of_term (fst (decompose_app c)) with 
        | Var id when List.exists (fun (i,_,_)-> i=id) (pf_hyps g) ->
 	   let id' = fresh_id [] id g in 
-	   tclTHENS (internal_cut id' (pf_type_of g term))
+	   tclTHENS (fun g -> internal_cut id' (pf_type_of g term) g)
 	     [ exact_no_check term; 
 	       tclTHEN (clear [id]) (rename_hyp [id',id]) ]
-       | _ -> tclTHENLAST (cut (pf_type_of g term)) (exact_no_check term))
+       | _ -> tclTHENLAST 
+                 (fun g -> cut (pf_type_of g term) g)
+                 (exact_no_check term))
     g
 
 (* Keeping only a few hypotheses *)
@@ -2208,7 +2210,7 @@ let mapi f l =
   mapi_aux f 0 l
 
 
-(* Instanciate all meta variables of elimclause using lid, some elts
+(* Instantiate all meta variables of elimclause using lid, some elts
    of lid are parameters (first ones), the other are
    arguments. Returns the clause obtained.  *)
 let recolle_clenv scheme lid elimclause gl = 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 014f6ffcd..3b4e8af21 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -163,3 +163,14 @@ apply H.
 try apply H.
 unfold ID; apply H0.
 Qed.
+
+(* Test coercion below product and on non meta-free terms in with bindings *)
+(* Cf wishes #1408 from E. Makarov *)
+
+Parameter bool_Prop :> bool -> Prop.
+Parameter r : bool -> bool -> bool.
+Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y.
+
+Theorem t : r true false.
+apply ax with (R := r).
+Qed.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index faeecdf9d..f5cee92c7 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -32,17 +32,17 @@ Section identity_is_a_congruence.
  Lemma sym_id : identity x y -> identity y x.
  Proof.
   destruct 1; trivial.
- Qed.
+ Defined.
 
  Lemma trans_id : identity x y -> identity y z -> identity x z.
  Proof.
   destruct 2; trivial.
- Qed.
+ Defined.
 
  Lemma congr_id : identity x y -> identity (f x) (f y).
  Proof.
   destruct 1; trivial.
- Qed.
+ Defined.
 
  Lemma sym_not_id : notT (identity x y) -> notT (identity y x).
  Proof.
diff --git a/toplevel/class.ml b/toplevel/class.ml
index f7d709480..7e5fc1297 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -27,28 +27,12 @@ open Nametab
 open Decl_kinds
 open Safe_typing
 
-let strength_min4 stre1 stre2 stre3 stre4 =
-  strength_min ((strength_min (stre1,stre2)),(strength_min (stre3,stre4)))
+let strength_min l = if List.mem Local l then Local else Global
 
 let id_of_varid c = match kind_of_term c with
   | Var id -> id
   | _ -> anomaly "class__id_of_varid"
 
-(* lf liste des variable dont depend la coercion f
-   lc liste des variable dont depend la classe source *)
-
-let rec stre_unif_cond = function
-  | ([],[]) -> Global
-  | (v::l,[]) -> variable_strength v
-  | ([],v::l) -> variable_strength v
-  | (v1::l1,v2::l2) ->
-      if v1=v2 then 
-	stre_unif_cond (l1,l2)
-      else
-	let stre1 = (variable_strength v1)
-	and stre2 = (variable_strength v2) in 
-	strength_min (stre1,stre2)
-
 (* Errors *)
 
 type coercion_error_kind =
@@ -98,9 +82,9 @@ let check_reference_arity ref =
 
 let check_arity = function
   | CL_FUN | CL_SORT -> ()
-  | CL_CONST sp -> check_reference_arity (ConstRef sp)
-  | CL_SECVAR sp -> check_reference_arity (VarRef sp)
-  | CL_IND sp  -> check_reference_arity (IndRef sp)
+  | CL_CONST cst -> check_reference_arity (ConstRef cst)
+  | CL_SECVAR id -> check_reference_arity (VarRef id)
+  | CL_IND kn -> check_reference_arity (IndRef kn)
 
 (* Coercions *)
 
@@ -184,20 +168,15 @@ let prods_of t =
   aux [] t
 
 let strength_of_cl = function 
-  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
-  | CL_SECVAR sp -> variable_strength sp
+  | CL_CONST kn -> Global
+  | CL_SECVAR id -> Local
   | _ -> Global
 
 let get_strength stre ref cls clt =
   let stres = strength_of_cl cls in
   let stret = strength_of_cl clt in
   let stref = strength_of_global ref in
-(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
-  let streunif = stre_unif_cond (s_vardep,f_vardep) in
- *)
-  let streunif = Global in
-  let stre' = strength_min4 stres stret stref streunif in
-  strength_min (stre,stre')
+  strength_min [stre;stres;stret;stref]
 
 (* coercion identité *)
 
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 34af2e326..3bbc2f043 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -22,28 +22,28 @@ open Nametab
 
 (* [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
    from [src] to [tg] *)
-val try_add_new_coercion_with_target : global_reference -> strength -> 
+val try_add_new_coercion_with_target : global_reference -> locality -> 
   source:cl_typ -> target:cl_typ ->  unit
 
 (* [try_add_new_coercion ref s] declares [ref], assumed to be of type
    [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : global_reference -> strength -> unit
+val try_add_new_coercion : global_reference -> locality -> unit
 
 (* [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
    transparent constant which unfolds to some class [tg]; it declares
    an identity coercion from [cst] to [tg], named something like
    ["Id_cst_tg"] *)
-val try_add_new_coercion_subclass : cl_typ -> strength -> unit
+val try_add_new_coercion_subclass : cl_typ -> locality -> unit
 
 (* [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
    from [src] to [tg] where the target is inferred from the type of [ref] *)
-val try_add_new_coercion_with_source : global_reference -> strength ->
+val try_add_new_coercion_with_source : global_reference -> locality ->
   source:cl_typ -> unit
 
 (* [try_add_new_identity_coercion id s src tg] enriches the
    environment with a new definition of name [id] declared as an
    identity coercion from [src] to [tg] *)
-val try_add_new_identity_coercion : identifier -> strength ->
+val try_add_new_identity_coercion : identifier -> locality ->
   source:cl_typ -> target:cl_typ -> unit
 
 val add_coercion_hook : Tacexpr.declaration_hook
diff --git a/toplevel/command.ml b/toplevel/command.ml
index bc8f6c9ee..8c368ec2e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -45,6 +45,7 @@ open Notation
 open Goptions
 open Mod_subst
 open Evd
+open Decls
 
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,default_binder_kind,a,b))
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,default_binder_kind,a,b))
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6b8fcdead..976677f8c 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -220,8 +220,8 @@ type vernac_expr =
       export_flag option * specif_flag option * lreference list
   | VernacImport of export_flag * lreference list
   | VernacCanonical of lreference
-  | VernacCoercion of strength * lreference * class_rawexpr * class_rawexpr
-  | VernacIdentityCoercion of strength * lident * 
+  | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr
+  | VernacIdentityCoercion of locality * lident * 
       class_rawexpr * class_rawexpr
 
   (* Type classes *)