diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 9 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
2 files changed, 5 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 4d67fef00..7f2ee2e87 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1410,17 +1410,16 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl = (* The set of hypotheses using x *) let depdecls = let test (id,_,c as dcl) = - if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then dcl - else failwith "caught" in - List.rev (map_succeed test (pf_hyps gl)) in + if id <> hyp && occur_var_in_decl (pf_env gl) x dcl then Some dcl + else None in + List.rev (List.map_filter test (pf_hyps gl)) in let dephyps = List.map (fun (id,_,_) -> id) depdecls in (* Decides if x appears in conclusion *) let depconcl = occur_var (pf_env gl) x (pf_concl gl) in (* The set of non-defined hypothesis: they must be abstracted, rewritten and reintroduced *) let abshyps = - map_succeed - (fun (id,v,_) -> if v=None then mkVar id else failwith "caught") + List.map_filter (function (id, None, _) -> Some (mkVar id) | _ -> None) depdecls in (* a tactic that either introduce an abstracted and rewritten hyp, or introduce a definition where x was replaced *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4ce382df2..057a268f5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1242,7 +1242,7 @@ let rec extract_ids ids = function let default_fresh_id = id_of_string "H" let interp_fresh_id ist env l = - let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in + let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in let id = if l = [] then default_fresh_id |