aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2018-03-06Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Maxime Dénès
2018-03-05Tweak comments to fix ocamldoc errorsmrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-05Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadMaxime Dénès
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04tactics: export e_reduct_in_conclEnrico Tassi
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-03-04Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Maxime Dénès
2018-03-04Merge PR #6676: [proofview] goals come with a stateMaxime Dénès
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-03-03[compat] Remove "Injection L2R Pattern Order"Emilio Jesus Gallego Arias
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
2018-03-01Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Hugo Herbelin
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20proofview: goals come with a stateEnrico Tassi
2018-02-19Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Maxime Dénès
2018-02-17Implement name mangling optionJasper Hugunin
2018-02-16apply_type: add option "typecheck" passed down to refineEnrico Tassi
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-29Merge PR #6493: [API] remove large file containing duplicate interfacesMaxime Dénès
2017-12-27[API] remove large file containing duplicate interfacesEnrico Tassi
2017-12-27Remove the local polymorphic flag hack.Maxime Dénès
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-12-11Remove deprecated option Tactic Compat Context.Théo Zimmermann
2017-12-11Remove deprecated option Dependent Propositions Eliminiation.Théo Zimmermann
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-07Getting rid of pf_matches in Hipattern.Pierre-Marie Pédrot
2017-11-30Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Maxime Dénès
2017-11-28In injection/inversion, consider all template-polymorphic types as injectable.Hugo Herbelin
2017-11-24Use Entries.constant_universes_entry more.Gaëtan Gilbert
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-11-24Separate checking univ_decls and obtaining universe binder names.Gaëtan Gilbert
2017-11-24Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 00:05:01 +0000