aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
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-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
2018-03-08Add an invariant on future goals in Proof.run_tactic.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08Proof engine: using save_future_goal when relevant.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-03-06Rename some universe minimizing "normalize" functions to "minimize"Gaëtan Gilbert
2018-03-06Deprecate UState aliases in Evd.Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.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 #6676: [proofview] goals come with a stateMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:56:54 +0000