aboutsummaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Expand)Author
2021-03-22Factorize goal selector handlingGaëtan Gilbert
2021-03-04Add noncritical constraint to exception catching in solve_constraintsLasse Blaauwbroek
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-01-13Avoid using "subgoals" in the UI, it means the same as "goals"Jim Fehrle
2021-01-04Fix behaviour of destruct after change of case representation.Pierre-Marie Pédrot
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-21Move evaluable_global_reference from Names to Tacred.Pierre-Marie Pédrot
2020-12-14Reuse the cache everywhere possible in Clenv.Pierre-Marie Pédrot
2020-12-14Store the metasubst cache in clenvs.Pierre-Marie Pédrot
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-12-14Cache meta access in meta_instance.Pierre-Marie Pédrot
2020-11-26[environ] [typing_flags] Introduce helper function to remove duplicate codeEmilio Jesus Gallego Arias
2020-11-26[proofs] Support per-definition typing-flags in interactive proofs.Emilio Jesus Gallego Arias
2020-11-16Deprecate `Grab Existential Variables` and `Existential` commandsMaxime Dénès
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-09-29Almost fully moving funind to new proof engine.Hugo Herbelin
2020-09-07Refine test for unresolved evars: not reachable from initial evarsMatthieu Sozeau
2020-09-07Remove dead code in clenv-generating functions.Pierre-Marie Pédrot
2020-09-04Remove a unused function from the Clenv API.Pierre-Marie Pédrot
2020-09-02Abstract type for allowed evarsMaxime Dénès
2020-09-02Replace `frozen` by `allowed` evars in evarconv, and delay themMaxime Dénès
2020-09-01Unify the shelvesMaxime Dénès
2020-08-31Update update_global_env usageGaëtan Gilbert
2020-08-26Wrap future goals into a moduleMaxime Dénès
2020-08-26Make future_goals stack explicit in the evarmapMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:13:51 +0000