Many improvements in tactics (and tactical) representation:

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

diff --git a/helm/gTopLevel/proofEngineStructuralRules.ml b/helm/gTopLevel/proofEngineStructuralRules.ml
index e3e024f34ce932c06d309b4e2aec49cd75540ef7..e01f95e9f02f121287fcc1416401878e1ac53263 100644 (file)
--- a/helm/gTopLevel/proofEngineStructuralRules.ml
+++ b/helm/gTopLevel/proofEngineStructuralRules.ml
@@ -25,22 +25,14 @@
 
 open ProofEngineTypes
 
-let clearbody ~status:(proof, goal) ~hyp =
+let clearbody ~hyp ~status:(proof, goal) =
  let module C = Cic in
   match hyp with
      None -> assert false
    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
    | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
-      let curi,metasenv,pbo,pty =
-       match proof with
-          None -> assert false
-        | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
-      in
-       let metano,_,_ =
-        match goal with
-           None -> assert false
-         | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
-       in
+      let curi,metasenv,pbo,pty = proof in
+       let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
         let string_of_name =
          function
             C.Name n -> n
@@ -95,22 +87,16 @@ let clearbody ~status:(proof, goal) ~hyp =
             | t -> t
           ) metasenv
         in
-         (Some (curi,metasenv',pbo,pty), goal)
+         (curi,metasenv',pbo,pty), [goal]
 
-let clear ~status:(proof, goal) ~hyp:hyp_to_clear =
+let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
  let module C = Cic in
   match hyp_to_clear with
      None -> assert false
    | Some (n_to_clear, _) ->
-      let curi,metasenv,pbo,pty =
-       match proof with
-          None -> assert false
-        | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
-      in
+      let curi,metasenv,pbo,pty = proof in
        let metano,context,ty =
-        match goal with
-           None -> assert false
-         | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
+        List.find (function (m,_,_) -> m=goal) metasenv
        in
         let string_of_name =
          function
@@ -159,5 +145,5 @@ let clear ~status:(proof, goal) ~hyp:hyp_to_clear =
             | t -> t
           ) metasenv
         in
-         (Some (curi,metasenv',pbo,pty), goal)
+         (curi,metasenv',pbo,pty), [goal]