aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-02Merge PR #7823: [tactics] function to gather undef evars of the goalPierre-Marie Pédrot
2018-09-29Replacing Refine.pr_constr by Termops.Internal.print_constr.Hugo Herbelin
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-24Merge PR #8464: Fix numeral notationsHugo Herbelin
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-09-17Ensure_prev_proof returns a proof that has underlying differences fromJim Fehrle
2018-09-11Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.Pierre-Marie Pédrot
2018-09-06Fixing #8270 (cbn was calling zeta even when not asked for).Hugo Herbelin
2018-09-06[pfedit] Fix master build due to merge conflictEmilio Jesus Gallego Arias
2018-09-06Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with ProgramMatthieu Sozeau
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-03Merge PR #7912: Simplify effects APIMaxime Dénès
2018-08-28Fix #7795: UGraph.AlreadyDeclared with ProgramGaëtan Gilbert
2018-08-27Add support for focusing on named goals using brackets.Théo Zimmermann
2018-08-15tacmach: function to gather undef evars of the goalMatthieu Sozeau
2018-07-05refine: obey the use_unification_heuristics flagMatthieu Sozeau
2018-06-27Swapping Context and Constr: defining declarations on constr in Constr.Hugo Herbelin
2018-06-26universes_of_constr don't include universes of monomorphic constantsGaëtan Gilbert
2018-06-24Further cleaning of the side-effect API.Pierre-Marie Pédrot
2018-06-24Share the role type between the implementations of side-effects.Pierre-Marie Pédrot
2018-06-15Do not allow spliting in res_pf, this is reserved for pretypingMatthieu Sozeau
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: move Tactypes to proofsEmilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-06-07Merge PR #6874: [econstr] Some minor tweaksPierre-Marie Pédrot
2018-06-04[econstr] Remove some Unsafe.to_constr use.Emilio Jesus Gallego Arias
2018-06-04Stronger invariants in unification signature.Pierre-Marie Pédrot
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Pierre-Marie Pédrot
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-17Split off Universes functions about substitutions and constraintsGaëtan Gilbert
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-14Deprecate Refiner [evar_map ref] exported functions.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-23Merge PR #7108: Legacy refiner handle eta-expanded case analysisPierre-Marie Pédrot
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-29Preparing old-style refine from logic.ml to deal with "Cases" proofHugo Herbelin
2018-03-27Congruence: getting rid of a detour by the compatibility layer of proof engine.Hugo Herbelin
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-08Cosmetic: add an expected newline in proof_global.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:58:52 +0000