diff options
| author | letouzey | 2013-03-12 23:59:25 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-12 23:59:25 +0000 |
| commit | 1126ec7c771e18644c361fcdf1f8d59d6b7f73e7 (patch) | |
| tree | 8385285f7fecab4dc2eaec5ab26ae79582bb13a2 /tactics | |
| parent | 66b098b04971f4bc08ce89afebdaec1772e3f73c (diff) | |
Hipattern : consider jmeq only when Logic.JMeq is loaded
Otherwise an Anomaly coming from Coqlib.find_reference is raised
and catched for the moment, but that will change soon.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16275 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hipattern.ml4 | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 9adb237a98..fadc50661a 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -352,9 +352,10 @@ let is_sigma_type t=op2bool (match_with_sigma_type t) let rec first_match matcher = function | [] -> raise PatternMatchingFailure - | (pat,build_set)::l -> - try (build_set (),matcher pat) - with PatternMatchingFailure -> first_match matcher l + | (pat,check,build_set)::l when check () -> + (try (build_set (),matcher pat) + with PatternMatchingFailure -> first_match matcher l) + | _::l -> first_match matcher l (*** Equality *) @@ -375,10 +376,13 @@ let match_eq eqn eq_pat = HeterogenousEq (t,x,t',x') | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms") +let no_check () = true +let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module + let equalities = - [coq_eq_pattern, build_coq_eq_data; - coq_jmeq_pattern, build_coq_jmeq_data; - coq_identity_pattern, build_coq_identity_data] + [coq_eq_pattern, no_check, build_coq_eq_data; + coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data; + coq_identity_pattern, no_check, build_coq_identity_data] let find_eq_data eqn = (* fails with PatternMatchingFailure *) first_match (match_eq eqn) equalities @@ -439,8 +443,8 @@ let match_sigma ex ex_pat = let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) first_match (match_sigma ex) - [coq_existT_pattern, build_sigma_type; - coq_exist_pattern, build_sigma] + [coq_existT_pattern, no_check, build_sigma_type; + coq_exist_pattern, no_check, build_sigma] (* Pattern "(sig ?1 ?2)" *) let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ] |