aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
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
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
2020-01-30Factorize export_private_constants + register_side_effectGaëtan Gilbert
2020-01-30[exn] Don't reraise in exception printersEmilio Jesus Gallego Arias
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
2020-01-27schemes: use rigid universesGaëtan Gilbert
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
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-12-18Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...Pierre-Marie Pédrot
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-12-13Use ~strict argument consistently in push_context/push_context_set intfsMatthieu Sozeau
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ...Pierre-Marie Pédrot
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-10Side-effect free wrapper around already declared schemes.Pierre-Marie Pédrot
2019-12-10Make explicit that users should not observe return values of scheme functions.Pierre-Marie Pédrot
2019-12-10Simplify internal flags in scheme declarations.Pierre-Marie Pédrot
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-11Do not export the internals of the prepare_hint function.Pierre-Marie Pédrot
2019-11-08Make [Proof_global.closed_proof_output] opaqueGaëtan Gilbert
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
2019-10-30Merge PR #10981: [abstract] Remove un-unused reference to `evar_map`Pierre-Marie Pédrot
2019-10-30Merge PR #10949: [declare] Provide helper for private constant inlining.Pierre-Marie Pédrot
2019-10-30Merge PR #10681: [declare] Make `proof_entry` a private type.Pierre-Marie Pédrot
2019-10-30Merge PR #10494: Show diffs in "Show Proof."Enrico Tassi
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-29[abstract] Remove un-unused reference to `evar_map`Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 02:55:42 +0000