X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FlogicalOperations.ml;h=277451bf42ed2774e99c46303822c03f47f1dec0;hb=e627ae3edfbe950b87069b625ec9317acaf03ec5;hp=b7c1a9bcfb6817d8e868010b255431b83b9bae35;hpb=c6a3408b6e603bed4f3d3c15f897b9007d98bb6f;p=helm.git

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index b7c1a9bcf..277451bf4 100644
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -73,7 +73,7 @@ let to_sequent id ids_to_terms ids_to_father_ids =
     let metasenv =
      match !P.proof with
         None -> assert false
-      | Some (metasenv,_,_) -> metasenv
+      | Some (_,metasenv,_,_) -> metasenv
     in
      let ty =
       CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term