diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-22 00:07:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-12 14:42:28 +0200 |
| commit | 368a25e4ef14512b00f5799e26c3f615bc540201 (patch) | |
| tree | 29602372307ff70f2a7b06f0a27609a73caa5666 /plugins/ltac/rewrite.ml | |
| parent | 36a98d55576ebdb106a55c3bd682961da8d77dee (diff) | |
[api] Misctypes removal: several moves:
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index b91315aca..cd04f4ae9 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -26,7 +26,7 @@ open Classes open Constrexpr open Globnames open Evd -open Misctypes +open Tactypes open Locus open Locusops open Decl_kinds @@ -1846,7 +1846,7 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) -let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) +let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) let proper_projection sigma r ty = let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in |