aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/contradiction.ml3
-rw-r--r--tactics/contradiction.mli2
-rw-r--r--tactics/elim.mli3
-rw-r--r--tactics/eqdecide.ml10
-rw-r--r--tactics/equality.ml12
-rw-r--r--tactics/equality.mli8
-rw-r--r--tactics/hints.ml16
-rw-r--r--tactics/hints.mli18
-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.ml14
-rw-r--r--tactics/tacticals.mli3
-rw-r--r--tactics/tactics.ml63
-rw-r--r--tactics/tactics.mli23
18 files changed, 121 insertions, 77 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 77fe314150..d7de6c4fb5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -99,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
Proofview.Goal.enter begin fun gl ->
let clenv, c = connect_hint_clenv poly c clenv gl in
let clenv = clenv_unique_resolver ~flags clenv gl in
- Clenvtac.clenv_refine false clenv
+ Clenvtac.clenv_refine clenv
end
let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4beeaaae05..773fc15208 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -207,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
with e -> Proofview.tclZERO e
in resolve >>= fun clenv' ->
- Clenvtac.clenv_refine with_evars ~with_classes:false clenv'
+ Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
end
let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index b92bc75bc3..e12063fd44 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 2b3a947586..4bb3263fb4 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/elim.mli b/tactics/elim.mli
index d6b67e5ba6..ddfac3f2cd 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -11,12 +11,11 @@
open Names
open EConstr
open Tacticals
-open Misctypes
open Tactypes
(** Eliminations tactics. *)
-val introCaseAssumsThen : evars_flag ->
+val introCaseAssumsThen : Tactics.evars_flag ->
(intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
branch_args -> unit Proofview.tactic
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 176701d992..832014a610 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 d7e697aed2..91c5774051 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -42,7 +42,7 @@ open Ind_tables
open Eqschemes
open Locus
open Locusops
-open Misctypes
+open Tactypes
open Proofview.Notations
open Unification
open Context.Named.Declaration
@@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let c1 = args.(arglen - 2) in
let c2 = args.(arglen - 1) in
let try_occ (evd', c') =
- Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
+ Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
in
let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
@@ -546,6 +546,12 @@ let apply_special_clear_request clear_flag f =
e when catchable_exception e -> tclIDTAC
end
+type multi =
+ | Precisely of int
+ | UpTo of int
+ | RepeatStar
+ | RepeatPlus
+
let general_multi_rewrite with_evars l cl tac =
let do1 l2r f =
Proofview.Goal.enter begin fun gl ->
@@ -1037,7 +1043,7 @@ let onEquality with_evars tac (c,lbindc) =
let t = type_of c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
- let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
+ let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
let eqn = clenv_type eq_clause' in
let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
tclTHEN
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ccf454c3e1..6f3e08ea02 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -15,8 +15,8 @@ open EConstr
open Environ
open Ind_tables
open Locus
-open Misctypes
open Tactypes
+open Tactics
(*i*)
type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
@@ -61,6 +61,12 @@ val general_rewrite_in :
val general_rewrite_clause :
orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
+type multi =
+ | Precisely of int
+ | UpTo of int
+ | RepeatStar
+ | RepeatPlus
+
val general_multi_rewrite :
evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
diff --git a/tactics/hints.ml b/tactics/hints.ml
index d49c8aaa56..85ff028249 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -125,7 +125,7 @@ type 'a hints_path_gen =
| PathEmpty
| PathEpsilon
-type pre_hints_path = Libnames.reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
type hints_path = GlobRef.t hints_path_gen
type hint_term =
@@ -157,7 +157,7 @@ type hint_entry = GlobRef.t option *
raw_hint hint_ast with_uid with_metadata
type reference_or_constr =
- | HintsReference of reference
+ | HintsReference of qualid
| HintsConstr of Constrexpr.constr_expr
type hint_mode =
@@ -167,12 +167,12 @@ type hint_mode =
type hints_expr =
| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
- | HintsResolveIFF of bool * reference list * int option
+ | HintsResolveIFF of bool * qualid list * int option
| HintsImmediate of reference_or_constr list
- | HintsUnfold of reference list
- | HintsTransparency of reference list * bool
- | HintsMode of reference * hint_mode list
- | HintsConstructors of reference list
+ | HintsUnfold of qualid list
+ | HintsTransparency of qualid list * bool
+ | HintsMode of qualid * hint_mode list
+ | HintsConstructors of qualid list
| HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
type import_level = [ `LAX | `WARN | `STRICT ]
@@ -1360,7 +1360,7 @@ let interp_hints poly =
let constr_hints_of_ind qid =
let ind = global_inductive_with_alias qid in
let mib,_ = Global.lookup_inductive ind in
- Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind";
+ Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
List.init (nconstructors ind)
(fun i -> let c = (ind,i+1) in
let gr = ConstructRef c in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e958f986e2..ca18f835a5 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -73,7 +73,7 @@ type search_entry
type hint_entry
type reference_or_constr =
- | HintsReference of Libnames.reference
+ | HintsReference of Libnames.qualid
| HintsConstr of Constrexpr.constr_expr
type hint_mode =
@@ -83,12 +83,12 @@ type hint_mode =
type hints_expr =
| HintsResolve of (hint_info_expr * bool * reference_or_constr) list
- | HintsResolveIFF of bool * Libnames.reference list * int option
+ | HintsResolveIFF of bool * Libnames.qualid list * int option
| HintsImmediate of reference_or_constr list
- | HintsUnfold of Libnames.reference list
- | HintsTransparency of Libnames.reference list * bool
- | HintsMode of Libnames.reference * hint_mode list
- | HintsConstructors of Libnames.reference list
+ | HintsUnfold of Libnames.qualid list
+ | HintsTransparency of Libnames.qualid list * bool
+ | HintsMode of Libnames.qualid * hint_mode list
+ | HintsConstructors of Libnames.qualid list
| HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
type 'a hints_path_gen =
@@ -99,7 +99,7 @@ type 'a hints_path_gen =
| PathEmpty
| PathEpsilon
-type pre_hints_path = Libnames.reference hints_path_gen
+type pre_hints_path = Libnames.qualid hints_path_gen
type hints_path = GlobRef.t hints_path_gen
val normalize_path : hints_path -> hints_path
@@ -110,9 +110,9 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t
val pp_hints_path : hints_path -> Pp.t
val pp_hint_mode : hint_mode -> Pp.t
val glob_hints_path_atom :
- Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
+ Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen
val glob_hints_path :
- Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen
+ Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen
module Hint_db :
sig
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5d264058ad..f9c4bed352 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 102b8e54d1..755494c2d2 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 9d4ffdd7b7..bbd1f3352a 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 2337a79016..f42e5a8b05 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 732d06f8af..f34c83ae72 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
@@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function
let compute_induction_names = compute_induction_names_gen true
(* Compute the let-in signature of case analysis or standard induction scheme *)
-let compute_constructor_signatures isrec ((_,k as ity),u) =
+let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
let rec analrec c recargs =
match Constr.kind c, recargs with
| Prod (_,_,c), recarg::rest ->
@@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
begin match Declareops.dest_recarg recarg with
| Norec | Imbr _ -> true :: rest
| Mrec (_,j) ->
- if isrec && Int.equal j k then true :: true :: rest
+ if rec_flag && Int.equal j k then true :: true :: rest
else true :: rest
end
| LetIn (_,_,_,c), rest -> false :: analrec c rest
@@ -636,7 +634,7 @@ module New = struct
(* Find the right elimination suffix corresponding to the sort of the goal *)
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
- isrec allnames tac predicate ind (c, t) =
+ rec_flag allnames tac predicate ind (c, t) =
Proofview.Goal.enter begin fun gl ->
let sigma, elim = mk_elim ind gl in
let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -665,7 +663,7 @@ module New = struct
(str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
in
let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
- let branchsigns = compute_constructor_signatures isrec ind in
+ let branchsigns = compute_constructor_signatures ~rec_flag ind in
let brnames = compute_induction_names_gen false branchsigns allnames in
let flags = Unification.elim_flags () in
let elimclause' =
@@ -688,7 +686,7 @@ module New = struct
in
let branchtacs = List.init (Array.length branchsigns) after_tac in
Proofview.tclTHEN
- (Clenvtac.clenv_refine false clenv')
+ (Clenvtac.clenv_refine clenv')
(Proofview.tclEXTEND [] tclIDTAC branchtacs)
end) end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cbaf691f1f..1e66c2b0b1 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -14,7 +14,6 @@ open EConstr
open Evd
open Proof_type
open Locus
-open Misctypes
open Tactypes
(** Tacticals i.e. functions from tactics to tactics. *)
@@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int ->
delayed_open_constr or_and_intro_pattern_expr ->
delayed_open_constr or_and_intro_pattern_expr
-val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array
+val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array
(** Useful for [as intro_pattern] modifier *)
val compute_induction_names :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b571b347d3..c430edf2e9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,7 +43,7 @@ open Pretype_errors
open Unification
open Locus
open Locusops
-open Misctypes
+open Tactypes
open Proofview.Notations
open Context.Named.Declaration
@@ -1153,6 +1153,11 @@ let tactic_infer_flags with_evar = {
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
+type evars_flag = bool (* true = pose evars false = fail on evars *)
+type rec_flag = bool (* true = recursive false = not recursive *)
+type advanced_flag = bool (* true = advanced false = basic *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
type 'a core_destruction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of lident
@@ -1281,7 +1286,7 @@ let do_replace id = function
let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
targetid id sigma0 clenv tac =
- let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
+ let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
let clenv =
if with_classes then
{ clenv with evd = Typeclasses.resolve_typeclasses
@@ -2258,7 +2263,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
let c = mkVar id in
let t = Tacmach.New.pf_unsafe_type_of gl c in
let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
- let branchsigns = compute_constructor_signatures false ind in
+ let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
let nv_with_let = Array.map List.length branchsigns in
let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
@@ -2645,6 +2650,15 @@ let insert_before decls lasthyp env =
push_named d env)
~init:(reset_context env) env
+let mk_eq_name env id {CAst.loc;v=ido} =
+ match ido with
+ | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env
+ | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env
+ | IntroIdentifier id ->
+ if List.mem id (ids_of_named_context (named_context env)) then
+ user_err ?loc (Id.print id ++ str" is already used.");
+ id
+
(* unsafe *)
let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
@@ -2654,14 +2668,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
else LocalAssum (id,t)
in
match with_eq with
- | Some (lr,{CAst.loc;v=ido}) ->
- let heq = match ido with
- | IntroAnonymous -> fresh_id_in_env (Id.Set.singleton id) (add_prefix "Heq" id) env
- | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env
- | IntroIdentifier id ->
- if List.mem id (ids_of_named_context (named_context env)) then
- user_err ?loc (Id.print id ++ str" is already used.");
- id in
+ | Some (lr,heq) ->
let eqdata = build_coq_eq_data () in
let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
let (sigma, eq) = Evd.fresh_global env sigma eqdata.eq in
@@ -4196,7 +4203,7 @@ let induction_tac with_evars params indvars elim =
let elimclause' = recolle_clenv i params indvars elimclause gl in
(* one last resolution (useless?) *)
let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
- Clenvtac.clenv_refine with_evars resolved
+ Clenvtac.clenv_refine ~with_evars resolved
end
(* Apply induction "in place" taking into account dependent
@@ -4396,7 +4403,8 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
match res with
| None ->
(* pattern not found *)
- let with_eq = Option.map (fun eq -> (false,eq)) eqname in
+ let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in
+ let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in
(* we restart using bindings after having tried type-class
resolution etc. on the term given by the user *)
let flags = tactic_infer_flags (with_evars && (* do not give a success semantics to edestruct on an open term yet *) false) in
@@ -4421,21 +4429,22 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
else Proofview.tclUNIT ();
if isrec then Proofview.cycle (-1) else Proofview.tclUNIT ()
])
- tac
+ (tac inhyps)
in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac
| Some (sigma', c) ->
(* pattern found *)
- let with_eq = Option.map (fun eq -> (false,eq)) eqname in
(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
let env = reset_with_named_context sign env in
+ let with_eq = Option.map (fun eq -> (false,mk_eq_name env id eq)) eqname in
+ let inhyps = if List.is_empty inhyps then inhyps else Option.fold_left (fun inhyps (_,heq) -> heq::inhyps) inhyps with_eq in
let tac =
Tacticals.New.tclTHENLIST [
Refine.refine ~typecheck:false begin fun sigma ->
mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
end;
- tac
+ (tac inhyps)
]
in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma') tac
@@ -4485,7 +4494,7 @@ let induction_gen clear_flag isrec with_evars elim
pose_induction_arg_then
isrec with_evars info_arg elim id arg t inhyps cls
(induction_with_atomization_of_ind_arg
- isrec with_evars elim names id inhyps)
+ isrec with_evars elim names id)
end
(* Induction on a list of arguments. First make induction arguments
@@ -5025,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac =
else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in
abstract_subproof ~opaque s gk tac
+let constr_eq ~strict x y =
+ let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in
+ let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Tacmach.New.pf_env gl in
+ let evd = Tacmach.New.project gl in
+ match EConstr.eq_constr_universes env evd x y with
+ | Some csts ->
+ let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in
+ if strict then
+ if Evd.check_constraints evd csts then Proofview.tclUNIT ()
+ else fail_universes
+ else
+ (match Evd.add_constraints evd csts with
+ | evd -> Proofview.Unsafe.tclEVARS evd
+ | exception Univ.UniverseInconsistency _ ->
+ fail_universes)
+ | None -> fail
+ end
+
let unify ?(state=full_transparent_state) x y =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b17330f133..57f20d2ff2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -18,7 +18,6 @@ open Clenv
open Redexpr
open Pattern
open Unification
-open Misctypes
open Tactypes
open Locus
open Ltac_pretype
@@ -56,8 +55,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] *)
@@ -91,6 +90,11 @@ val intros_clearing : bool list -> unit Proofview.tactic
val try_intros_until :
(Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic
+type evars_flag = bool (* true = pose evars false = fail on evars *)
+type rec_flag = bool (* true = recursive false = not recursive *)
+type advanced_flag = bool (* true = advanced false = basic *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
(** Apply a tactic on a quantified hypothesis, an hypothesis in context
or a term with bindings *)
@@ -117,11 +121,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 +192,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
@@ -405,6 +409,11 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -
(** {6 Other tactics. } *)
+(** Syntactic equality up to universes. With [strict] the universe
+ constraints must be already true to succeed, without [strict] they
+ are added to the evar map. *)
+val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
+
val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:51:45 +0000