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

3 files changed, 8 insertions, 6 deletions

diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 5402e61209..e3e90c7ca6 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 b19df1aee9..dc8ff2b9cd 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 34c2f690c0..d3f7cc5f15 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 =