aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2018-05-25Merge pull request #7569 from ppedrot/clean-newringAssia Mahboubi
2018-05-25Merge PR #7524: [ssr] fix after to_constr ~abort_on_undefined_evars was addedMaxime Dénès
2018-05-24[tactics] Remove anonymous fix/cofix form.Emilio Jesus Gallego Arias
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Pierre-Marie Pédrot
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
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-21Simplify the newring hack.Pierre-Marie Pédrot
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-17Merge PR #7359: Reduce usage of evar_map referencesPierre-Marie Pédrot
2018-05-16[ssr] fix after to_constr ~abort_on_undefined_evars was addedEnrico Tassi
2018-05-15Merge PR #7213: Do not compute constr matching context if not used.Matthieu Sozeau
2018-05-14Deprecate Typing.e_* functionsGaëtan Gilbert
2018-05-14Deprecate Refiner [evar_map ref] exported functions.Gaëtan Gilbert
2018-05-11Deprecate Evarconv.e_conv,e_cumulGaëtan Gilbert
2018-05-11Convert clear_hyps_in_evi to state passing style.Gaëtan Gilbert
2018-05-11Deprecate most evarutil evdref functionsGaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-30Merge PR #6935: Separate universe minimization and evar normalization functionsPierre-Marie Pédrot
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
2018-04-23Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"Pierre-Marie Pédrot
2018-04-17Deprecate mixing univ minimization and evm normalization functions.Gaëtan Gilbert
2018-04-16Merge PR #7125: Adding ML headers in setoid_ringMaxime Dénès
2018-04-16Merge PR #7237: [ssr] fix delayed clears (fix #7045)Maxime Dénès
2018-04-13Making tactic-in-term aware of "Set Ltac Debug".Hugo Herbelin
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-04-13Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output contain...Pierre-Marie Pédrot
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
2018-04-12Merge PR #7202: Correction of ugly message described in #4667Pierre Courtieu
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-04-12Merge PR #7107: Fixes #7100: lost of main file location in case of Ltac failu...Pierre-Marie Pédrot
2018-04-11Correction of ugly message described in #4667Julien Forest
2018-04-10Do not compute constr matching context if not used.Pierre-Marie Pédrot
2018-04-09change error message in #5147Julien Forest
2018-04-09removing uggly error message of #5147Julien Forest
2018-04-09Merge PR #7165: [ssr] check cleared hyps do exist (fix #7050)Maxime Dénès
2018-04-06Merge PR #6960: [api] Move some types to their proper module.Pierre-Marie Pédrot
2018-04-05Merge PR #7016: Make parsing independent of the cumulativity flag.Enrico Tassi
2018-04-04Fixing #7100 (lost of main file location in case of Ltac failure in other file).Hugo Herbelin
2018-04-04ssr: check cleared hyps do exist (fix #7050)Enrico Tassi
2018-04-02Fix #6404 - Print tactics called by ML tacticsJason Gross
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-30Adding some headers, by consistency of style.Hugo Herbelin
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
2018-03-27Congruence: typography in a comment.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:16:25 +0000