* Many improvements

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

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index b7c1a9bcfb6817d8e868010b255431b83b9bae35..277451bf42ed2774e99c46303822c03f47f1dec0 100644 (file)
--- 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