diff options
Diffstat (limited to 'tactics/hipattern.ml4')
| -rw-r--r-- | tactics/hipattern.ml4 | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 130e66720..a8bcec288 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -387,12 +387,6 @@ let match_eq eqn eq_pat = let no_check () = true let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module -let build_coq_jmeq_data_in env = - build_coq_jmeq_data (), Univ.ContextSet.empty - -let build_coq_identity_data_in env = - build_coq_identity_data (), Univ.ContextSet.empty - let equalities = [coq_eq_pattern, no_check, build_coq_eq_data; coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data; @@ -442,11 +436,6 @@ let dest_nf_eq gls eqn = (*** Sigma-types *) -(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) -let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ] -let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref -let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref - let match_sigma ex = match kind_of_term ex with | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f -> |