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, 18 insertions, 1 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 47b10e6dd0..262214c3a7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -603,11 +603,28 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
     let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in
     List.fold_left
       (fun (isevars,b as p) (pbty,t1,t2) ->
-        if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
+	if b then conv_algo env isevars pbty t1 t2 else p) (isevars,true)
       pbs
   with e when precatchable_exception e ->
     (isevars,false)
 
+
+(* [check_evars] fails if some unresolved evar remains *)
+(* it assumes that the defined existentials have already been substituted *)
+
+let check_evars env initial_sigma isevars c =
+  let sigma = evars_of isevars in
+  let c = nf_evar sigma c 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
+
 (* Operations on value/type constraints *)
 
 type type_constraint_type = (int * int) option * constr