* Many improvements

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

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 664425062757e788f615ef3dbe49d8cf2d726bd0..277451bf42ed2774e99c46303822c03f47f1dec0 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -57,6 +57,8 @@ let get_context ids_to_terms ids_to_father_ids =
 
 exception NotImplemented;;
 
+(* It returns true iff the proof has been perforated, i.e. if a subterm *)
+(* has been changed into a meta.                                        *)
 let to_sequent id ids_to_terms ids_to_father_ids =
  let module P = ProofEngine in
   let term = Hashtbl.find ids_to_terms id in
@@ -68,6 +70,20 @@ let to_sequent id ids_to_terms ids_to_father_ids =
        | P.Definition,_,_ -> raise NotImplemented
      ) context
    in
-    let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in
-     ((context,ty) : ProofEngine.sequent)
+    let metasenv =
+     match !P.proof with
+        None -> assert false
+      | Some (_,metasenv,_,_) -> metasenv
+    in
+     let ty =
+      CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term
+     in
+      let (meta,perforated) =
+       (* If the selected term is already a meta, we return it. *)
+       (* Otherwise, we are trying to refine a non-meta term... *)
+       match term with
+          Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
+        | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
+      in
+       perforated
 ;;