aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
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-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
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-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
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-22Fix #6591: anomaly when using selectors outside of a proof.Cyprien Mangin
2018-01-11Force polymorphic definitions to have no internal constraints.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 15:37:02 +0000