aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacticals API using EConstr.Pierre-Marie Pédrot
2017-02-14Clenv API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacmach API using EConstr.Pierre-Marie Pédrot
2017-02-14Refine API using EConstr.Pierre-Marie Pédrot
2017-02-14Goal API using EConstr.Pierre-Marie Pédrot
2017-02-14Cleaning up opening of the EConstr module in pretyping folder.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules.
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Pretyping API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Constr_matching 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-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarsolve API using EConstr.Pierre-Marie Pédrot
2017-02-14Find_subterm 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-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-28Merge remote-tracking branch 'github/pr/321' into v8.6Maxime Dénès
Was PR#321: Handling of section variables in hints
2016-10-26Using msg_info for info_auto and info_eauto (PR #324).Hugo Herbelin
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-25Merge remote-tracking branch 'github/pr/338' into v8.5Maxime Dénès
Was PR#338: Remove warning now that info_auto is fixed.
2016-10-25Remove warning now that info_auto is fixed.Théo Zimmermann
Removes a warning dating from 8.5 signaling that info_auto and info_trivial are broken and advising to use Info 1 auto instead. Now, these tactics are fixed and thus they can be used again. They do not do exactly the same thing as Info 1 auto and may be more useful for the learner.
2016-10-25Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."Maxime Dénès
This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses.
2016-10-22Fixing printing of generic arguments of tag "var".Hugo Herbelin
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-17Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-15Still a problem with debug auto printing.Hugo Herbelin
"msg_debug (mt())" is not identity, so we return back to how it was done in 8.4, contracting a repeated pattern-matching into one.
2016-10-15One more little bug in the output of "debug auto".Hugo Herbelin
Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"...
2016-10-14Fix bug #5139: Anomalies should not be caught by || / try.Pierre-Marie Pédrot
There was a catch-all clause in the tclORELSE0 function. We now only catch noncritical exceptions.
2016-10-14Fixing printing of info_auto broken since 0091c528 (2014).Hugo Herbelin
2016-10-14Fixing English typography for colon.Hugo Herbelin
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-10-10Fix #4416: - Incorrect "Error: Incorrect number of goals"Arnaud Spiwack
In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-07Fix bug #4464: "Anomaly: variable H' unbound. Please report.".Pierre-Marie Pédrot
We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel.
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Clean up type classes flags and update compat file.Maxime Dénès
2016-10-03Merge remote-tracking branch 'github/pr/263' into v8.6Maxime Dénès
Was PR#263: Fast lookup in named contexts
2016-10-03fixing bug 4609: document an option governing the generation of equalitiesYves Bertot
between proofs in tactic injection, with a side-effect on inversion.
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 20:34:08 +0000