Report de l'heuristique d'unification premier ordre flexible/rigide

en dernière étape de la procédure d'unification
- Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution
  de l'unification premier ordre flexible/rigide
- Déplacement check_evars dans Evarutil
Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ?
(cf exemples d'application dans test-suite/success/evars.v)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 33 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 738a951470..bb973b71ee 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -114,8 +114,6 @@ sig
 
   val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
 
-  val check_evars : env -> evar_map -> evar_defs ref -> constr -> unit
-
   (*i*)
   (* Internal of Pretyping...
    * Unused outside, but useful for debugging
@@ -634,35 +632,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	  (pretype_type empty_valcon env isevars lvar c).utj_val in
       nf_evar (evars_of !isevars) c'
 
-  (* [check_evars] fails if some unresolved evar remains *)
-  (* it assumes that the defined existentials have already been substituted
-     (should be done in unsafe_infer and unsafe_infer_type) *)
-
-  let check_evars env initial_sigma isevars c =
-    let sigma = evars_of !isevars in
-    let rec proc_rec c =
-      match kind_of_term c with
-	| Evar (ev,args) ->
-            assert (Evd.mem sigma ev);
-	    if not (Evd.mem initial_sigma ev) then
-              let (loc,k) = evar_source ev !isevars in
-		error_unsolvable_implicit loc env sigma k
-	| _ -> iter_constr proc_rec c
-    in
-      proc_rec c(*;
-		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-		  if pbs <> [] then begin
-		  pperrnl
-		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-		  prlist_with_sep fnl
-		  (fun  (pb,c1,c2) ->
-		  Termops.print_constr c1 ++
-		  (if pb=Reduction.CUMUL then str " <="++ spc()
-		  else str" =="++spc()) ++
-		  Termops.print_constr c2)
-		  pbs ++ fnl())
-		  end*)
-
   (* TODO: comment faire remonter l'information si le typage a resolu des
      variables du sigma original. il faudrait que la fonction de typage
      retourne aussi le nouveau sigma...
@@ -671,7 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let understand_judgment sigma env c =
     let isevars = ref (create_evar_defs sigma) in
     let j = pretype empty_tycon env isevars ([],[]) c in
-    let j = j_nf_evar (evars_of !isevars) j in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let j = j_nf_evar (evars_of isevars) j in
       check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
 
@@ -688,8 +658,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let isevars = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen isevars env lvar kind c in
+    let isevars,_ = consider_remaining_unif_problems env !isevars in
+    let c = nf_evar (evars_of isevars) c in
       if fail_evar then check_evars env sigma isevars c;
-      !isevars, c
+      isevars, c
 
   (** Entry points of the high-level type synthesis algorithm *)