(* 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
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)
) 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 *)
(*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
| _ -> i
) newmetasenv []
in
- let newproof = Some (uri,metasenv',bo',ty) in
+ let newproof = uri,metasenv',bo',ty in
(newproof, metasenv')