aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaëtan Gilbert
Instead of various termops and globnames aliases.
2020-02-06unsafe_type_of -> type_of in Sequent.extend_with_auto_hintsGaëtan Gilbert
+ fix evar leak in caller
2020-02-06Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)Gaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Leminv.lemInvGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Equality.inject_if_homogenous_dependent_pairGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Equality.build_injrecGaëtan Gilbert
2020-02-06Remove useless unification in Equality.sig_clausal_formGaëtan Gilbert
We unify [w_type = type of w] with [a], but [w] was created with type [a]. This code was introduced in eab11e537905472fdcc3257bc9913df82c82b3e4 to fix #2255, AFAICT only the [minimal_free_rels_rec] part is necessary.
2020-02-06unsafe_type_of -> (get_)type_of in ↵Gaëtan Gilbert
Equality.{discrEq,minimal_free_rels_rec,sig_clausal_form}
2020-02-06unsafe_type_of -> get_type_of in Inv.raw_inversionGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Elim.induction_trailerGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Elim.general_decomposer + pf_apply in ifOnHypGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Autorewrite.{find,decompose}_applied_relationGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Contradiction.contradiction_termGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Class_tactics.autoapplyGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tacticals.elimination_thenGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tacticals.general_elim_then_usingGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Hipattern.extract_eq_argsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Hints.make_trivialGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.prove_transitivityGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.symmetry_inGaëtan Gilbert
I'm a bit dubious about the tclENV in match_with_equation but let's leave it for now.
2020-02-06unsafe_type_of -> type_of in Tactics.induction_gen_l + fix bad envGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tactics.is_functional_inductionGaëtan Gilbert
2020-02-06Fix evar map leak in Tactics.find_induction_typeGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.given_elimGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.guess_elimGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.abstract_argsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Tactics.atomize_param_of_ind_thenGaëtan Gilbert
Not 100% sure about this one TBH, this function is messy.
2020-02-06unsafe_type_of -> type_of in Tactics.rewrite_hyp_then (+ tclEVARSTHEN)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.intro_or_and_patternGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.intro_decomp_eq (hipattern changes)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.cut_and_applyGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.find_eliminatorGaëtan Gilbert
2020-02-06unsafe_type_of + match -> sort_of in Tactics.cutGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.change_on_subtermGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.convert_conclGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Eqdecide (2 occurrences)Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Eauto.e_give_exactGaëtan Gilbert
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-01-30Factorize export_private_constants + register_side_effectGaëtan Gilbert
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
This behaviour seems a bit dubious and it is indeed not needed, also such re-raises seem like they will mess with the backtrace.
2020-01-30export_private_constants doesn't use the [constr in_univ_ctx] argumentGaëtan Gilbert
2020-01-30Merge PR #11307: Remove the hacks relying on hardwired libobject tags.Maxime Dénès
Reviewed-by: maximedenes
2020-01-27schemes: use rigid universesGaëtan Gilbert
so for instance ~~~coq Set Printing All. Set Printing Universes. Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . Lemma bla@{u v|u < v} : foo@{u v} -> False. Proof. induction 1. Qed. ~~~ works.
2020-01-21Translating a comment from French to English.Hugo Herbelin
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
The type of h is reconstructed to look as much as the initial type of h as possible.
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
The patch is done in a minimal way. The hacks are turned into a new kind of safer hacks, but hacks nonetheless. They should go away at some point, but the current patch is focussed on the removal of Libobject cruft, not making the dirty code of its upper-layer callers any cleaner.
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ↵Pierre-Marie Pédrot
~strict flag Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: ppedrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
There are no users in Coq but maybe some plugin wants it so don't completely remove it
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:48:05 +0000