diff options
Diffstat (limited to 'tactics/hipattern.ml')
-rw-r--r-- | tactics/hipattern.ml | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 39c2bd8f7..8e7648704 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -125,6 +125,17 @@ let is_unit_type t = op2bool (match_with_unit_type t) inductive binary relation R, so that R has only one constructor establishing its reflexivity. *) +(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *) +let x = Name (id_of_string "x") +let y = Name (id_of_string "y") +let name_A = Name (id_of_string "A") +let coq_refl_rel1_pattern = + PProd + (name_A, PMeta None, + PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|]))) +let coq_refl_rel2_pattern = + PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|])) + let match_with_equation t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with @@ -133,8 +144,8 @@ let match_with_equation t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if nconstr = 1 && - (is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0) || - is_matching (build_coq_refl_rel1_pattern ()) constr_types.(0)) + (is_matching coq_refl_rel1_pattern constr_types.(0) || + is_matching coq_refl_rel1_pattern constr_types.(0)) then Some (hdapp,args) else @@ -143,9 +154,13 @@ let match_with_equation t = let is_equation t = op2bool (match_with_equation t) +(* ["(?1 -> ?2)"] *) +let imp a b = PProd (Anonymous, a, b) +let coq_arrow_pattern = imp (PMeta (Some 1)) (PMeta (Some 2)) + let match_with_nottype t = try - match matches (build_coq_arrow_pattern ()) t with + match matches coq_arrow_pattern t with | [(1,arg);(2,mind)] -> if is_empty_type mind then Some (mind,arg) else None | _ -> anomaly "Incorrect pattern matching" |