aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.ml
AgeCommit message (Expand)Author
2021-04-19Check for existence before using `Global.lookup_constant` instead of catching...Lasse Blaauwbroek
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-10-21Similar introduction of a Construct module in the Names API.Pierre-Marie Pédrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-04Remove the last use of clenv_fchain in Equality.Pierre-Marie Pédrot
2020-09-04Inline the last use of apply_on_clause in Equality.Pierre-Marie Pédrot
2020-09-04Remove a useless use of clenv_fchain in Equality.Pierre-Marie Pédrot
2020-09-03Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay themPierre-Marie Pédrot
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-09-02Document the Equality.equality type in the ML file.Pierre-Marie Pédrot
2020-09-02Remove redundant data from the equality eliminator datatype.Pierre-Marie Pédrot
2020-09-02Use a dedicated type for equality elimination.Pierre-Marie Pédrot
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
2020-08-18Tactic replace: adding support for registration of an equality in Type.Hugo Herbelin
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:38:23 +0000