aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/contradiction.ml3
-rw-r--r--tactics/contradiction.mli2
-rw-r--r--tactics/eqdecide.ml10
-rw-r--r--tactics/equality.ml1
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/inv.ml14
-rw-r--r--tactics/inv.mli1
-rw-r--r--tactics/leminv.mli2
-rw-r--r--tactics/tacticals.ml4
-rw-r--r--tactics/tactics.ml1
-rw-r--r--tactics/tactics.mli12
11 files changed, 25 insertions, 27 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index b92bc75bc..e12063fd4 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -14,7 +14,6 @@ open Hipattern
open Tactics
open Coqlib
open Reductionops
-open Misctypes
open Proofview.Notations
module NamedDecl = Context.Named.Declaration
@@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) =
else
Proofview.tclORELSE
begin
- if lbind = NoBindings then
+ if lbind = Tactypes.NoBindings then
filter_hyp (fun c -> is_negation_of env sigma typ c)
(fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
else
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 2b3a94758..4bb3263fb 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open EConstr
-open Misctypes
+open Tactypes
val absurd : constr -> unit Proofview.tactic
val contradiction : constr with_bindings option -> unit Proofview.tactic
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 176701d99..832014a61 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -24,11 +24,11 @@ open Tactics
open Tacticals.New
open Auto
open Constr_matching
-open Misctypes
open Hipattern
open Proofview.Notations
open Tacmach.New
open Coqlib
+open Tactypes
(* This file containts the implementation of the tactics ``Decide
Equality'' and ``Compare''. They can be used to decide the
@@ -58,14 +58,14 @@ let clear_last =
let choose_eq eqonleft =
if eqonleft then
- left_with_bindings false Misctypes.NoBindings
+ left_with_bindings false NoBindings
else
- right_with_bindings false Misctypes.NoBindings
+ right_with_bindings false NoBindings
let choose_noteq eqonleft =
if eqonleft then
- right_with_bindings false Misctypes.NoBindings
+ right_with_bindings false NoBindings
else
- left_with_bindings false Misctypes.NoBindings
+ left_with_bindings false NoBindings
(* A surgical generalize which selects the right occurrences by hand *)
(* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index c91758787..1033c56c9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -43,6 +43,7 @@ open Eqschemes
open Locus
open Locusops
open Misctypes
+open Tactypes
open Proofview.Notations
open Unification
open Context.Named.Declaration
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5d264058a..f9c4bed35 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,7 +263,7 @@ open Evar_kinds
let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
let mkGApp f args = DAst.make @@ GApp (f, args)
let mkGHole = DAst.make @@
- GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
+ GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None)
let mkGProd id c1 c2 = DAst.make @@
GProd (Name (Id.of_string id), Explicit, c1, c2)
let mkGArrow c1 c2 = DAst.make @@
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 102b8e54d..755494c2d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -26,7 +26,7 @@ open Tacticals.New
open Tactics
open Elim
open Equality
-open Misctypes
+open Tactypes
open Proofview.Notations
module NamedDecl = Context.Named.Declaration
@@ -332,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function
(tacfun (get_names allow_conj a))
(tclMAP_i allow_conj (n-1) tacfun l)
-let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
+let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id
(* invariant: ProjectAndApply is responsible for erasing the clause
which it is given as input
@@ -375,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
[if as_mode then clear [id] else tclIDTAC;
(tclMAP_i (false,false) neqns (function (idopt,_) ->
tclTRY (tclTHEN
- (intro_move_avoid idopt avoid MoveLast)
+ (intro_move_avoid idopt avoid Logic.MoveLast)
(* try again to substitute and if still not a variable after *)
(* decomposition, arbitrarily try to rewrite RL !? *)
(tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
@@ -404,7 +404,7 @@ let nLastDecls i tac =
let rewrite_equations as_mode othin neqns names ba =
Proofview.Goal.enter begin fun gl ->
let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
- let first_eq = ref MoveLast in
+ let first_eq = ref Logic.MoveLast in
let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
match othin with
| Some thin ->
@@ -416,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba =
(nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
tclMAP_i (true,false) neqns (fun (idopt,names) ->
(tclTHEN
- (intro_move_avoid idopt avoid MoveLast)
+ (intro_move_avoid idopt avoid Logic.MoveLast)
(onLastHypId (fun id ->
tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
names;
tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
- intro_move idopt (if thin then MoveLast else !first_eq))
+ intro_move idopt (if thin then Logic.MoveLast else !first_eq))
nodepids;
(tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
| None ->
(* simple inversion *)
if as_mode then
tclMAP_i (false,true) neqns (fun (idopt,_) ->
- intro_move idopt MoveLast) names
+ intro_move idopt Logic.MoveLast) names
else
(tclTHENLIST
[tclDO neqns intro;
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 9d4ffdd7b..bbd1f3352 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -10,7 +10,6 @@
open Names
open EConstr
-open Misctypes
open Tactypes
type inversion_status = Dep of constr option | NoDep
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 2337a7901..f42e5a8b0 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -11,7 +11,7 @@
open Names
open EConstr
open Constrexpr
-open Misctypes
+open Tactypes
val lemInv_clause :
quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 732d06f8a..53a02f89b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -159,8 +159,6 @@ type branch_assumptions = {
ba : branch_args; (* the branch args *)
assums : named_context} (* the list of assumptions introduced *)
-open Misctypes
-
let fix_empty_or_and_pattern nv l =
(* 1- The syntax does not distinguish between "[ ]" for one clause with no
names and "[ ]" for no clause at all *)
@@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
if Int.equal p p1 then
IntroAndPattern
- (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l)
+ (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l)
else
names
else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b571b347d..cf07532c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -44,6 +44,7 @@ open Unification
open Locus
open Locusops
open Misctypes
+open Tactypes
open Proofview.Notations
open Context.Named.Declaration
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b17330f13..086442e42 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -56,8 +56,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list
val intro : unit Proofview.tactic
val introf : unit Proofview.tactic
-val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic
-val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic
+val intro_move : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic
+val intro_move_avoid : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic
(** [intro_avoiding idl] acts as intro but prevents the new Id.t
to belong to [idl] *)
@@ -117,11 +117,11 @@ val use_clear_hyp_by_default : unit -> bool
(** {6 Introduction tactics with eliminations. } *)
val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
-val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns ->
+val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns ->
+val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns ->
unit Proofview.tactic
-val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr ->
unit Proofview.tactic
(** Implements user-level "intros", with [] standing for "**" *)
@@ -188,7 +188,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic
-val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic
+val move_hyp : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic
val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic
val revert : Id.t list -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 10:04:14 +0000