essai de typage des instantiations d\'evars

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

1 files changed, 13 insertions, 1 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 098c3e095..6101396a4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -989,7 +989,19 @@ let check_evars fail_evar env initial_sigma isevars c =
 	       error_unsolvable_implicit loc env sigma k)
       | _ -> iter_constr proc_rec c      
   in
-  proc_rec c
+  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