Experimental commit: definitions are now allowed in contexts. As a consequence,

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 49510a9dde1dc7f9a2480df7d7a7afc11caf686f..47c416d8b60b9ad472098d883f4cacf2f2026345 100644 (file)
--- 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