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

7 files changed, 15 insertions, 16 deletions

diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index b825262005..a4dc0eacd3 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 172c7479c2..6b17e7396a 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 afe7fc6d2b..7d4eb72a97 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 0f9331ff52..9eac4fbaed 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 3551b262c8..1bd5bb970c 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 5515320f0a..6ea000f5b6 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 649139f356..7e3a1bd410 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