aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2020-04-15[tmp] Compat API for CIEmilio Jesus Gallego Arias
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proofs] Move pfedit to `proofs`Emilio Jesus Gallego Arias
2020-04-15[declare] [abstract] Do evars check in declare_abstractEmilio Jesus Gallego Arias
2020-04-15[declare] Mark APIs as scheduled for removal; remove a couple.Emilio Jesus Gallego Arias
2020-04-15[proof] [abstract] Move internal declaration code to `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-04-14Merge PR #11820: Partial importsMaxime Dénès
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-10[sideeff] Don't use polymorphic equality to check for empty side-effectsEmilio Jesus Gallego Arias
2020-04-10[proof] Introduce `prepare_proof` to improve normalization workflow.Emilio Jesus Gallego Arias
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ...Hugo Herbelin
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-31[proof] Improve comment and argument name.Emilio Jesus Gallego Arias
2020-03-31[proof] [stm] Force `opaque` in `close_future_proof`Emilio Jesus Gallego Arias
2020-03-31[proof] Remove unused parameter in the delayed save path.Emilio Jesus Gallego Arias
2020-03-31[proof] Fixme on unused return type.Emilio Jesus Gallego Arias
2020-03-31[proof] Remove internal wrapper in Proof_globalEmilio Jesus Gallego Arias
2020-03-31[proof] Minor refactorings in Proof_globalEmilio Jesus Gallego Arias
2020-03-31[proof] Split return_proof in partial and regular versions.Emilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IEmilio Jesus Gallego Arias
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
2020-03-25[proof] Start of mutual definition save refactoring.Emilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[pfedit] Labelize sign parameterEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[declare] Remove one use of inline_private_constantsEmilio Jesus Gallego Arias
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-13Fixing a non-protected try-with in class_tactics.ml.Hugo Herbelin
2020-03-13Deprecation of catchable_exception, to be replaced by noncritical in try-with.Hugo Herbelin
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-08[exn] [nit] Remove not very useful re-raises.Emilio Jesus Gallego Arias
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-03-02Refine patch for clearer scoping of evar_mapMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:02:38 +0000