From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- tactics/contradiction.ml | 3 +-- tactics/contradiction.mli | 2 +- tactics/eqdecide.ml | 10 +++++----- tactics/equality.ml | 1 + tactics/hipattern.ml | 2 +- tactics/inv.ml | 14 +++++++------- tactics/inv.mli | 1 - tactics/leminv.mli | 2 +- tactics/tacticals.ml | 4 +--- tactics/tactics.ml | 1 + tactics/tactics.mli | 12 ++++++------ 11 files changed, 25 insertions(+), 27 deletions(-) (limited to 'tactics') 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 -- cgit v1.2.3