diff options
Diffstat (limited to 'tactics/tactic_matching.ml')
| -rw-r--r-- | tactics/tactic_matching.ml | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml index 80786058..004492e7 100644 --- a/tactics/tactic_matching.ml +++ b/tactics/tactic_matching.ml @@ -11,6 +11,7 @@ open Names open Tacexpr +open Context.Named.Declaration (** [t] is the type of matching successes. It ultimately contains a {!Tacexpr.glob_tactic_expr} representing the left-hand side of the @@ -102,7 +103,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) = (merged, Id.Map.merge merge lcm lm) let matching_error = - Errors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") + CErrors.UserError ("tactic matching" , Pp.str "No matching clauses for match.") let imatching_error = (matching_error, Exninfo.null) @@ -278,9 +279,10 @@ module PatternMatching (E:StaticEnvironment) = struct [hyps]. Tries the hypotheses in order. For each success returns the name of the matched hypothesis. *) let hyp_match_type hypname pat hyps = - pick hyps >>= fun (id,b,hyp) -> - let refresh = not (Option.is_empty b) in - pattern_match_term refresh pat hyp () <*> + pick hyps >>= fun decl -> + let id = get_id decl in + let refresh = is_local_def decl in + pattern_match_term refresh pat (get_type decl) () <*> put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> return id @@ -290,12 +292,12 @@ module PatternMatching (E:StaticEnvironment) = struct success returns the name of the matched hypothesis. *) let hyp_match_body_and_type hypname bodypat typepat hyps = pick hyps >>= function - | (id,Some body,hyp) -> + | LocalDef (id,body,hyp) -> pattern_match_term false bodypat body () <*> pattern_match_term true typepat hyp () <*> put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*> return id - | (id,None,hyp) -> fail + | LocalAssum (id,hyp) -> fail (** [hyp_match pat hyps] dispatches to {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether @@ -317,7 +319,7 @@ module PatternMatching (E:StaticEnvironment) = struct (* spiwack: alternatively it is possible to return the list with the matched hypothesis removed directly in [hyp_match]. *) - let select_matched_hyp (id,_,_) = Id.equal id matched_hyp in + let select_matched_hyp decl = Id.equal (get_id decl) matched_hyp in let hyps = CList.remove_first select_matched_hyp hyps in hyp_pattern_list_match pats hyps lhs | [] -> return lhs |