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

10 files changed, 139 insertions, 119 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5b0c2eb367..0d7e3d611c 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 dd51ee970a..c1a62b34fd 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 ed9d779ad7..e7423c748b 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 729bd84f1f..bd023721ae 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 5476a4820c..00735d8746 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 3adf749f07..ddc3654dc7 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 352d3021d9..71c6bb0dc3 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 e118a659e9..e825b3f488 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 c5e9dff8b4..b140ad51aa 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 9156623f50..1b8f9ccd8b 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]                       *)