aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Expand)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2021-03-04Cleanup internal hint locality handlingGaëtan Gilbert
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
2021-01-04Change the representation of kernel case.Pierre-Marie Pédrot
2020-12-14Make the clenv type private and provide a creation function.Pierre-Marie Pédrot
2020-11-15Implement export locality for the remaining Hint commands.Pierre-Marie Pédrot
2020-11-04Do not try to be clever for term-as-hint interpretation.Pierre-Marie Pédrot
2020-11-04Opacify the Hints.hint_term type.Pierre-Marie Pédrot
2020-11-04Encapsulate the last use of IsConstr in the Hints API.Pierre-Marie Pédrot
2020-11-04Further API cleanup after the removal of forward hints.Pierre-Marie Pédrot
2020-09-13Statically ensure that only polymophic hint terms come with a context.Pierre-Marie Pédrot
2020-08-31Perform an inversion of control in hint validation for eapply.Pierre-Marie Pédrot
2020-08-20Do not store the transparent state in delayed dnets.Pierre-Marie Pédrot
2020-08-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
2020-08-19Replace Hints.head_constr_bound with Hints.head_bound.Pierre-Marie Pédrot
2020-08-19Simplify the computation of the head global for hint patterns.Pierre-Marie Pédrot
2020-08-19Ensure statically that Hint Extern comes with a pattern.Pierre-Marie Pédrot
2020-08-14Do not precompute hint dnets eagerly.Pierre-Marie Pédrot
2020-08-13Merge PR #12720: Factor code related to class hint clenvHugo Herbelin
2020-08-12Cosmetic changes as suggested by SkySkimmer.Pierre-Marie Pédrot
2020-08-12Split the uses of connect_hint_clenv into two different functions.Pierre-Marie Pédrot
2020-08-12Export a dedicated function that applies immediately a hint.Pierre-Marie Pédrot
2020-08-12Move connect_hint_clenv from Auto to Hints.Pierre-Marie Pédrot
2020-07-27Do not rely on higher-order interfaces for patterns in dnets.Pierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
2020-06-19Wrap the content of full hints into a record.Pierre-Marie Pédrot
2020-06-19Remove access to hint section variables.Pierre-Marie Pédrot
2020-06-19Opacify the type of hint metadata.Pierre-Marie Pédrot
2020-06-19Remove dead code in the Hints API.Pierre-Marie Pédrot
2020-06-19Do not export flags in Hints.make_resolves.Pierre-Marie Pédrot
2020-05-16Factorize code in hint declaration.Pierre-Marie Pédrot
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
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-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-02-28Move the warning code out of the parser.Pierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Hints.make_trivialGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:38:24 +0000