diff options
| author | Pierre-Marie Pédrot | 2018-06-13 10:25:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-13 10:25:20 +0200 |
| commit | c1d690443589a457b18b39b7003ccb762bcf401f (patch) | |
| tree | 723f70ee85dc2b646ea19d8afa03972d21c78820 /plugins/ltac/extratactics.ml4 | |
| parent | 573c6d76d343cadaa68b5851fdebba937153c24d (diff) | |
| parent | 1dd682b1cafd64dd902e1ae6ea738192eb9b26db (diff) | |
Merge PR #7677: [api] Remove Misctypes
Diffstat (limited to 'plugins/ltac/extratactics.ml4')
| -rw-r--r-- | plugins/ltac/extratactics.ml4 | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index cb7183638e..f2899ab63c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -24,7 +24,8 @@ open CErrors open Util open Termops open Equality -open Misctypes +open Namegen +open Tactypes open Proofview.Notations open Vernacinterp @@ -604,7 +605,7 @@ let subst_var_with_hole occ tid t = (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous), - Misctypes.IntroAnonymous, None))) + IntroAnonymous, None))) else x | _ -> map_glob_constr_left_to_right substrec x in let t' = substrec t @@ -615,13 +616,13 @@ let subst_hole_with_term occ tc t = let locref = ref 0 in let occref = ref occ in let rec substrec c = match DAst.get c with - | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) -> + | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) -> decr occref; if Int.equal !occref 0 then tc else (incr locref; DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s)) + GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s)) | _ -> map_glob_constr_left_to_right substrec c in substrec t |