diff options
| author | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
| commit | 915554785ffed11370f5d700d11a8b5614408096 (patch) | |
| tree | 4b5b4120c896cf99c863fab4fd5e1ec22af20d53 /tactics | |
| parent | ebe133a0df0656de82a566c4f1673257f60f7c0c (diff) | |
| parent | 9f47342d890dc3ef7f4950004513a47d940af5ca (diff) | |
Merge PR #6186: [api] Miscellaneous consolidation.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 1 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 6a9cd7e206..de98f63823 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -9,7 +9,6 @@ open Equality open Names open Pp -open Term open Constr open Termops open CErrors diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 75fae6647d..8e851375a6 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -160,7 +160,7 @@ let test_strict_disjunction n lc = let open Term in Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with - | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) + | [LocalAssum (_,c)] -> Constr.isRel c && Int.equal (Constr.destRel c) (n - i) | _ -> false) 0 lc let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = |