diff options
| author | ppedrot | 2013-09-27 19:20:27 +0000 |
|---|---|---|
| committer | ppedrot | 2013-09-27 19:20:27 +0000 |
| commit | 11ca3113365639136cf65a74c345080a9434e69b (patch) | |
| tree | da263c149cd1e90bde14768088730e48e78e4776 /tactics | |
| parent | ee2f85396fa0cef65bc4295b5ac6c259e83df134 (diff) | |
Removing a bunch of generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/termdn.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index ee296c5e5a..40834be365 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -285,7 +285,7 @@ let make_autogoal_hints = let sign = pf_filtered_hyps g in match freeze () with | Some (onlyc, sign', hints) - when onlyc = only_classes && + when (onlyc : bool) == only_classes && Environ.eq_named_context_val sign sign' -> hints | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in unfreeze (Some (only_classes, sign, hints)); hints diff --git a/tactics/equality.ml b/tactics/equality.ml index 04d6b9d8e8..a53910f343 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1186,7 +1186,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause gl = errorlabstrm "Equality.inj" (str"Nothing to inject.") | Inr posns -> try inject_if_homogenous_dependent_pair env sigma u gl - with e when (Errors.noncritical e || e = Not_dep_pair) -> + with Not_dep_pair as e | e when Errors.noncritical e -> inject_at_positions env sigma l2r u eq_clause posns (tac (clenv_value eq_clause)) gl @@ -1208,7 +1208,7 @@ let postInjEqTac ipats c n = let injEq ipats = let l2r = - if use_injection_pattern_l2r_order () && ipats <> None then true else false + if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false in injEqThen (postInjEqTac ipats) l2r diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4a60f6559a..81ee6f19a0 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1511,7 +1511,7 @@ let assert_as first ipat c gl = match kind_of_term (pf_hnf_type_of gl c) with | Sort s -> let id,tac = prepare_intros s ipat gl in - let repl = allow_replace c ipat <> None in + let repl = not (Option.is_empty (allow_replace c ipat)) in tclTHENS ((if first then internal_cut_gen else internal_cut_rev_gen) repl id c) (if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl diff --git a/tactics/termdn.ml b/tactics/termdn.ml index becd19a669..432a4123b6 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -22,7 +22,7 @@ struct module X = struct type t = constr_pattern - let compare = Pervasives.compare + let compare = Pervasives.compare (** FIXME *) end type term_label = |