diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 16 | ||||
| -rw-r--r-- | tactics/hints.mli | 18 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 20 | ||||
| -rw-r--r-- | tactics/tactics.mli | 5 |
5 files changed, 44 insertions, 19 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index d49c8aaa5..85ff02824 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 e958f986e..ca18f835a 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/tacticals.ml b/tactics/tacticals.ml index f34c83ae7..837865e64 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -753,8 +753,8 @@ module New = struct let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with - | None -> true,gl_make_elim - | Some _ -> false,gl_make_case_dep + | NotRecord -> true,gl_make_elim + | FakeRecord | PrimRecord _ -> false,gl_make_case_dep in general_elim_then_using mkelim isrec None tac None ind (c, t) end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 67a812987..928530744 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5040,6 +5040,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 8d4302450..57f20d2ff 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -409,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 |