aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrelim.ml
AgeCommit message (Expand)Author
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2020-08-27Remove a call to the old refiner in ssr.Pierre-Marie Pédrot
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-07-16[gramlib] Remove legacy located exception wrapper in favor of standard infras...Emilio Jesus Gallego Arias
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tacticsPierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Remove legacy layer in SSR.Pierre-Marie Pédrot
2020-05-03Further port of the SSR tactics.Pierre-Marie Pédrot
2020-05-03Further port of the SSR code.Pierre-Marie Pédrot
2020-05-03Wrap ssr tactics into V82.tactic.Pierre-Marie Pédrot
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-05[cleanup] remove useless EConstr qualificationsEnrico Tassi
2020-02-02Move kind_of_type from the kernel to ssr.Pierre-Marie Pédrot
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-05-23Fixing typos - Part 2JPR
2019-04-10Remove calls to global env from indrecMaxime Dénès
2019-03-27[plugins] [ssr] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-26Merge PR #9489: [ssr] avoid HO unification to perform truncation analysy in elimMaxime Dénès
2019-03-25[ssr] avoid HO unif when doing truncation analysisEnrico Tassi
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-11-21Merge PR #8985: [gramlib] [build] Switch make-based system to packed gramlibEnrico Tassi
2018-11-21[legacy proof engine] Remove some cruft.Emilio Jesus Gallego Arias
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
2018-11-14ssr: elim: do resolve TC once and forall at the very endEnrico Tassi
2018-10-24[ssreflect] Better use of CoqlibVincent Laporte
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-09-04[ssr] guard all `try pf_unify_HO` with CErrors.noncriticalEnrico Tassi
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-06ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)Enrico Tassi
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04ssr: ipats: V82.tactic ~nf_evars:false everywhereEnrico Tassi
2018-03-04ssr: rewrite Ssripats and Ssrview in the tactic monadEnrico Tassi
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-10-26Passing around the flag for injection so that tactics calling inj atHugo Herbelin
2017-07-17[API] Remove `open API` in ml files in favor of `-open API` flag.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:21:39 +0000