diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-11-22 15:12:55 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-11-22 15:12:55 +0100 |
| commit | 34ed0bb1b198ff92436177b303e2e6b4db931816 (patch) | |
| tree | 858bf017baca3f3a2ace309166f826942b8c909d | |
| parent | 1abae19d5688b987b19efba8bcac8577892fcd27 (diff) | |
Remove some occurrences of obsolete operators
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
3 files changed, 4 insertions, 4 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 725508965..c317413a3 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -478,7 +478,7 @@ let raw_inversion inv_kind id status names = let (elim_predicate,neqns) = make_inv_predicate env sigma indf realargs id status concl in let (cut_concl,case_tac) = - if status != NoDep & (dependent c concl) then + if status != NoDep && (dependent c concl) then Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), Tacticals.New.case_then_using else diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 6c2ed5287..2b9e6d1d8 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -75,7 +75,7 @@ let catching_error call_trace fail e = | Some inner_trace -> inner_trace, e | None -> [], e in - if List.is_empty call_trace & List.is_empty inner_trace then fail e + if List.is_empty call_trace && List.is_empty inner_trace then fail e else begin assert (Errors.noncritical e); (* preserved invariant *) let new_trace = inner_trace @ call_trace in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2f52c8b7a..720d46201 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3324,8 +3324,8 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = | _ -> [] in match kind_of_term c with | Var id when not (mem_named_context id (Global.named_context())) - & lbind == NoBindings & not with_evars & Option.is_empty eqname - & not (has_selected_occurrences cls) -> + && lbind == NoBindings && not with_evars && Option.is_empty eqname + && not (has_selected_occurrences cls) -> Tacticals.New.tclTHEN (Proofview.V82.tactic (clear_unselected_context id inhyps cls)) (induction_with_atomization_of_ind_arg |