aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-06unsafe_type_of -> get_type_of in ComProgramFixpoint.build_wellfoundedGaëtan Gilbert
We typecheck it literally the previous line...
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-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-06replace RList by list RYves Bertot
add an overlay for coquelicot remove functions from RList: In, Rlength, cons_Rlist, app_RList because they are essentially the same as In, length, app, and map from List (beware that the order of arguments changes for map, and the In function contains reversed equalities). adds deprecation warnings for Rlist and Rlength adds deprecated notations for RList.cons and RList.nil
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-05Add --fuzz, --real, --user to timing scriptsJason Gross
- Add a `--fuzz` option to `make-both-single-timing-files.py` Passing `--fuzz=N` allows differences in character locations of up to `N` characters when matching lines in per-line timing diffs. The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`. See also the discussion at https://github.com/coq/coq/pull/11076#pullrequestreview-324791139 - Allow passing `--real` to per-file timing scripts and `--user` to per-line timing script. This allows easily comparing real times instead of user ones (or vice versa). - Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build - We also now use argparse rather than a hand-rolled argument parser; there were getting to be too many combinations of options. - Fix the ordering of columns in Coq's build system; this is the equivalent of #8167 for Coq's build system. Fixes #11301 Supersedes / closes #11022 Supersedes / closes #11230
2020-02-05Merge PR #11414: Remove the Tactic menu from CoqIDE.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-02-05Remove a dubious part of the checker code relying on a universe contextPierre-Marie Pédrot
data from a part where it should never access it.
2020-02-05Store the template polymorphic context inside the TemplateArity node.Pierre-Marie Pédrot
This was the only part in the kernel that really relied on the contents of the Monomorphic node.
2020-02-05[cleanup] remove useless EConstr qualificationsEnrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 16:10:10 +0000