aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-06unsafe_type_of -> type_of in Pretyping.pretype_refGaëtan Gilbert
We already thread the evar map
2020-02-06unsafe_type_of -> type_of in Unification.applyHeadGaëtan Gilbert
We already thread the evar map
2020-02-06unsafe_type_of -> type_of in Tacred.pattern_occsGaëtan Gilbert
This function already returns the evar map so no problem.
2020-02-06unsafe_type_of -> get_type_of in casesGaëtan Gilbert
It goes in an error message so should be fine.
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
Reviewed-by: ppedrot
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive ↵Pierre-Marie Pédrot
notations (+ a fix about locations) Reviewed-by: ppedrot
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-05Merge PR #11511: Delay lifting in Evarsolve aliasing.Enrico Tassi
Reviewed-by: gares
2020-02-04Merge PR #11491: Small side effect cleanupPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-02-04Merge PR #11513: Test for #5617: Primitive projections confuse the ↵Gaëtan Gilbert
termination checker. Reviewed-by: SkySkimmer
2020-02-04Merge PR #11514: add regression test for liaPierre-Marie Pédrot
Reviewed-by: fajb
2020-02-04Merge PR #11474: Fix efficiency regression #11436Vincent Laporte
Ack-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: vbgl
2020-02-03add regression test for liaAndres Erbsen
2020-02-03Merge PR #11508: [ci] [fiat-crypto] Use the pinned bedrock2Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-03Test for #5617: Primitive projections confuse the termination checker.Pierre-Marie Pédrot
Fixes #5617.
2020-02-03Do not return a full term in Evarsolve alias expansion.Pierre-Marie Pédrot
The only user is merely observing whether this can be an rel / var alias.
2020-02-03Delay lifting in Evarsolve aliasing.Pierre-Marie Pédrot
It turns out that eagerly computing the lift of huge terms when it is not used is not great for performance. Fixes part of #11488.
2020-02-03Merge PR #11497: [opam] Don't disable native compute in opam.dev fileGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-03Merge PR #11493: [makefile] Ignore _build_boot directoryGaëtan Gilbert
Reviewed-by: SkySkimmer
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:51:48 +0000