diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 08:11:07 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-22 11:33:57 +0100 |
commit | 88afd8a9853c772b6b1681c7ae208e55e7daacbe (patch) | |
tree | 7561c915ee289a94ea29ff5538fbafa004f4e901 /tactics | |
parent | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (diff) |
[api] Deprecate Term destructors, move to Constr
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
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 6a9cd7e20..de98f6382 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 75fae6647..8e851375a 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 = |