Many improvements in tactics (and tactical) representation:

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

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
index 7e5f3a4b19b6468f527f5c67702991dbbbe12962..d191340ea88b8882a290c100bfc51b0d95f07714 100644 (file)
--- a/helm/gTopLevel/proofEngineHelpers.ml
+++ b/helm/gTopLevel/proofEngineHelpers.ml
@@ -40,11 +40,7 @@ let identity_relocation_list_for_metavariable canonical_context =
 (* Returns the first meta whose number is above the *)
 (* number of the higher meta.                       *)
 let new_meta ~proof =
- let metasenv =
-  match proof with
-     None -> assert false
-   | Some (_,metasenv,_,_) -> metasenv
- in
+ let (_,metasenv,_,_) = proof in
   let rec aux =
    function
       None,[] -> 1
@@ -55,11 +51,7 @@ let new_meta ~proof =
    1 + aux (None,metasenv)
 
 let subst_meta_in_proof proof meta term newmetasenv =
- let (uri,metasenv,bo,ty) =
-  match proof with
-     None -> assert false
-   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
- in
+ let uri,metasenv,bo,ty = proof in
   let subst_in = CicUnification.apply_subst [meta,term] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
@@ -79,7 +71,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
       ) metasenv'
     in
      let bo' = subst_in bo in
-      let newproof = Some (uri,metasenv'',bo',ty) in
+      let newproof = uri,metasenv'',bo',ty in
        (newproof, metasenv'')
 
 (*CSC: commento vecchio *)
@@ -95,11 +87,7 @@ let subst_meta_in_proof proof meta term newmetasenv =
 (*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
 (*CSC: [newmetasenv].                                             *)
 let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,bo,ty) =
-  match proof with
-     None -> assert false
-   | Some (uri,_,bo,ty) -> uri,bo,ty
- in
+ let (uri,_,bo,ty) = proof in
   let bo' = subst_in bo in
   let metasenv' =
    List.fold_right
@@ -118,6 +106,6 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
        | _ -> i
     ) newmetasenv []
   in
-   let newproof = Some (uri,metasenv',bo',ty) in
+   let newproof = uri,metasenv',bo',ty in
     (newproof, metasenv')