X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=47c416d8b60b9ad472098d883f4cacf2f2026345;hb=200d1d63cd5fc282df768f97d33214c1572c89da;hp=49510a9dde1dc7f9a2480df7d7a7afc11caf686f;hpb=756c1e676368d9addc75438bce97a71e34287f18;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 49510a9dd..47c416d8b 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -582,7 +582,10 @@ let save rendering_window () =
  match !ProofEngine.proof with
     None -> assert false
   | Some (uri,[],bo,ty) ->
-     if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then
+     if
+      CicReduction.are_convertible []
+       (CicTypeChecker.type_of_aux' [] [] bo) ty
+     then
       begin
        (*CSC: Wrong: [] is just plainly wrong *)
        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in