aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2020-08-26Better encapsulation of future goalsMaxime Dénès
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-12Code simplification around hint manipulation in Class_tactics.Pierre-Marie Pédrot
2020-08-06Actually use the default instance stored inside named_context_val.Pierre-Marie Pédrot
2020-08-06Use the evarinfo-stored identity substitution where applicable.Pierre-Marie Pédrot
2020-08-06Store the default evar instance inside the evar info.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_evar_instance from the API.Pierre-Marie Pédrot
2020-07-08Remove Evarutil.new_pure_evar_full from the API.Pierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-29Refining out the Refiner.Pierre-Marie Pédrot
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-06-29Remove Refiner.refiner.Pierre-Marie Pédrot
2020-06-29Remove the deprecated functions from refiner, moving them to Tacticals.Pierre-Marie Pédrot
2020-06-26[declare] Remove mutual internals from Info.t structure.Emilio Jesus Gallego Arias
2020-06-25Merge PR #12579: Simplify Clenv APIEmilio Jesus Gallego Arias
2020-06-24Remove the catchable-exception related functions.Pierre-Marie Pédrot
2020-06-24Simplify Clenv.clenv_pose_metas_as_evars.Pierre-Marie Pédrot
2020-06-24Actually remove internal API from the Clenv mli.Pierre-Marie Pédrot
2020-06-24Merge Clenvtac into Clenv.Pierre-Marie Pédrot
2020-06-24Remove all uses of clenv_unique_resolver.Pierre-Marie Pédrot
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-12Remove a unused legacy tactic from Clenv.Pierre-Marie Pédrot
2020-05-12Write the outermost part of the legacy refiner directly in the monad.Pierre-Marie Pédrot
2020-05-12Clean up the legacy refiner implementation.Pierre-Marie Pédrot
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
2020-05-12Wrap the legacy refiner type into the Logic API.Pierre-Marie Pédrot
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
2020-05-07Deprecate the legacy tacticals from module Refiner.Pierre-Marie Pédrot
2020-05-05Fix GeoCoq slowdown.Pierre-Marie Pédrot
2020-05-03Remove a very specific low-level tactical from Refiner.Pierre-Marie Pédrot
2020-05-03Wrap Refiner.refiner in the tactic monad.Pierre-Marie Pédrot
2020-05-03Remove a critical call to V82.tactic in Clenvtac.Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
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-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-30Merge PR #11921: Remove some cruft from Reductionops API.Gaëtan Gilbert
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-28Remove some cruft from Reductionops API.Pierre-Marie Pédrot
2020-03-22[proof] Deprecate unused tacmach functions.Emilio Jesus Gallego Arias
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:13:12 +0000