aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Collapse)Author
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-02Remove unused module definition after merging PR#592.Maxime Dénès
2017-05-02Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.Maxime Dénès
2017-04-30Fix bug #5501: Universe polymorphism breaks proof involving auto.Pierre-Marie Pédrot
A universe substitution was lacking as the normalized evar map was dropped.
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
Today, both modes are controlled by a single flag, however this is a bit misleading as is_silent really means "quiet", that is to say `coqc -q` whereas "verbose" is Coq normal operation. We also restore proper behavior of goal printing in coqtop on quiet mode, thanks to @Matafou for the report.
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Quick hack to fix interpretation of patterns in Ltac.Pierre-Marie Pédrot
Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip through the pretyper, and relies on suspicious flagging of evars in the evar source field to recognize original pattern holes. After the pattern_of_constr function was made evar-insensitive, it expanded evars that were solved by magical side-effects of the pretyper, even if it hadn't been asked to perform any heuristics. We backtrack on the insensitivity of the pattern_of_constr function. This may have a performance penalty in other dubious code, e.g. hints. In the long run we should get rid of the pattern_of_constr function.
2017-02-14Removing a subtle nf_enter in Class_tactics.Pierre-Marie Pédrot
The underlying hint mode implementation was not using the evar-insensitive API so that it resulted in strange bugs.
2017-02-14Chasing a few unsafe constr coercions.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers related to printing.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers in RetypingPierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2017-02-14Goal API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Patternops API using EConstr.Pierre-Marie Pédrot
2017-02-14Typing API using EConstr.Pierre-Marie Pédrot
2017-02-14Retyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Fix bug #5232: proper globalization of hints pathsMatthieu Sozeau
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
Was PR#339: Documenting type class options, typeclasses eauto
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
Was PR#336: Remove v62
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-25Remove v62 from the codebase.Théo Zimmermann
2016-10-21sections/hints: prevent Not_found in get_type_ofMatthieu Sozeau
due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared.
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-14Using "simple apply" and "simple eapply" in the trace of auto.Hugo Herbelin
This is more precise and probably clearer (see e.g. thread "Understanding auto" on coq-club).
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Fix bug #4958: [debug auto] should specify hint databases.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-08Unplugging Pptactic from Ppvernac.Pierre-Marie Pédrot
2016-09-08Making Hints generic in the use of external tactics.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions. If multiple modules define a function with a same name, e.g.: Context.{Rel,Named}.get_type those calls were prefixed with a corresponding prefix to make sure that it is obvious which function is being called.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 15:15:58 +0000