aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
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-06unsafe_type_of -> type_of in Pretyping.pretype_refGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Unification.applyHeadGaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tacred.pattern_occsGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in casesGaëtan Gilbert
2020-02-06replace RList by list RYves Bertot
2020-02-06Merge PR #11458: Don't install doc_grammarEnrico Tassi
2020-02-06Merge PR #11478: Nicer kernel universe error for inductivesPierre-Marie Pédrot
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive notati...Pierre-Marie Pédrot
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
2020-02-05Remove a dubious part of the checker code relying on a universe contextPierre-Marie Pédrot
2020-02-05Store the template polymorphic context inside the TemplateArity node.Pierre-Marie Pédrot
2020-02-05[cleanup] remove useless EConstr qualificationsEnrico Tassi
2020-02-05Merge PR #11511: Delay lifting in Evarsolve aliasing.Enrico Tassi
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
2020-02-04Remove `unsafe_type_of` from `Coercion`Maxime Dénès
2020-02-04Apply suggestions from HugoSimonBoulier
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
2020-02-04Non maximal implicits: add overlays for several librariesSimonBoulier
2020-02-04Non maximal implicits: entry in dev/doc/changes.mdSimonBoulier
2020-02-04Add changelog for non maximal implicit argsSimonBoulier
2020-02-04Update doc for non max implicit argumentsSimonBoulier
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-02-04Merge PR #11513: Test for #5617: Primitive projections confuse the terminatio...Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 06:14:45 +0000