aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-12Standardize constr -> globref operations to use destRef/isRef/isRefXGaë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
2020-02-06unsafe_type_of -> (get_)type_of in Equality.{discrEq,minimal_free_rels_rec,si...Gaëtan Gilbert
2020-02-06unsafe_type_of -> type_of in Tactics.intro_decomp_eq (hipattern changes)Gaëtan Gilbert
2019-11-30Actually deprecate the `cutrewrite` tacticMaxime Dénès
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-14Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
2019-05-10Make the check flag of conversion functions mandatory.Pierre-Marie Pédrot
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-03-25Fix #9652: rewrite fails to detect lack of progressGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-06-26Remove Sorts.contentsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:18:31 +0000