X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineHelpers.ml;h=d191340ea88b8882a290c100bfc51b0d95f07714;hb=4720c6af414c4a834a994fdb404fda2d0c04fc03;hp=7e5f3a4b19b6468f527f5c67702991dbbbe12962;hpb=6fa39011a07aaaf20b99929965ba93df8a81cdbb;p=helm.git

diff --git a/helm/gTopLevel/proofEngineHelpers.ml b/helm/gTopLevel/proofEngineHelpers.ml
index 7e5f3a4b1..d191340ea 100644
--- 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')