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

4 files changed, 5 insertions, 5 deletions

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