diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/hipattern.ml4 | 17 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
4 files changed, 21 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index cbcf5993c..641e274af 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -116,13 +116,13 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_ let sigma = Evd.merge sigma (project gl) in let ctype = get_type_of env sigma c' in let rels, t = decompose_prod (whd_betaiotazeta ctype) in - match match_with_equation t with + match match_with_equality_type t with | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *) leibniz_rewrite_ebindings_clause cls lft2rgt sigma c' l with_evars gl hdcncl | None -> let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in let _,t' = splay_prod env' sigma t in (* Search for underlying eq *) - match match_with_equation t' with + match match_with_equality_type t' with | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *) if l = NoBindings && !is_applied_setoid_relation t then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 4145a8dcc..9e0281855 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -121,8 +121,8 @@ let match_with_unit_type t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in let zero_args c = - nb_prod c = mib.mind_nparams in - if nconstr = 1 && array_for_all zero_args constr_types then + nb_prod c = mib.mind_nparams in + if nconstr = 1 && zero_args constr_types.(0) then Some hdapp else None @@ -157,6 +157,19 @@ let match_with_equation t = let is_equation t = op2bool (match_with_equation t) +let match_with_equality_type t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind when args <> [] -> + let (mib,mip) = Global.lookup_inductive ind in + let nconstr = Array.length mip.mind_consnames in + if nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0 + then + Some (hdapp,args) + else + None + | _ -> None + let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ] let match_arrow_pattern t = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 6dde098cf..ce1c70e5a 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -69,6 +69,9 @@ val is_unit_type : testing_function val match_with_equation : (constr * constr list) matching_function val is_equation : testing_function +(* type with only one constructor, no arguments and at least one dependency *) +val match_with_equality_type : (constr * constr list) matching_function + val match_with_nottype : (constr * constr) matching_function val is_nottype : testing_function diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e0f5a3a42..da4d95eaa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2900,7 +2900,7 @@ let reflexivity_red allowred gl = let concl = if not allowred then pf_concl gl else whd_betadeltaiota (pf_env gl) (project gl) (pf_concl gl) in - match match_with_equation concl with + match match_with_equality_type concl with | None -> None | Some _ -> Some (one_constructor 1 NoBindings) |