aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mli
Commit message (Collapse)AuthorAge
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
|
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
|
* Adding an "as" clause to specialize.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | | | | Comments -------- - The tactic specialize conveys a somehow intuitive reasoning concept and I would support continuing maintaining it even if the design comes in my opinion with some oddities. (Note that the experience of MathComp and SSReflect also suggests that specialize is an interesting concept in itself). There are two variants to specialize: - specialize (H args) with H an hypothesis looks natural: we specialize H with extra arguments and the "as pattern" clause comes naturally as an extension of it, destructuring the result using the pattern. - specialize term with bindings makes the choice of fully applying the term filling missing expressions with bindings and to then behave as generalize. Wouldn't we like a more fine-grained approach and the result to remain in the context? In this second case, the "as" clause works as if the term were posed in the context with "pose proof".
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
| | | | | simplifying and generalizing the grammar entries for injection, discriminate and simplify_eq.
* A cleaning phase around delayed induction arg + exporting force_induction_arg.Gravatar Hugo Herbelin2016-06-18
|
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
| | | | | | | | | | | | | | | | | | | | | In pat%constr, creating new evars is now allowed only if "eintros" is given, i.e. "intros" checks that no evars are created, and similarly e.g. for "injection ... as ... pat%constr". The form "eintros [...]" or "eintros ->" with the case analysis or rewrite creating evars is now also supported. This is not a commitment to say that it is good to have an e- modifier to tactics. It is just to be consistent with the existing convention. It seems to me that the "no e-" variants are good for beginners. However, expert might prefer to use the e-variants by default. Opinions from teachers and users would be useful. To be possibly done: do that [= ...] work on hypotheses with side conditions or parameters based on the idea that they apply the full injection and not only the restriction of it to goals which are exactly an equality, as it is today.
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
| | | | | | simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
|
* Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
| | | | | | It is indeed confusing, as it has little to do with the proper refine defined in the New submodule. Legacy code relying on it should call the Logic or Tacmach modules instead.
* Put the "move" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-17
|
* Put the "change" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "generalize dependent" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "cofix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "*_cast_no_check" tactics in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "fix" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "exact_constr" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
|
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
| | | | This reverts commit bde36d4b00185065628324d8ca71994f84eae244.
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
| | | | | | allows for a simpler re-printing of assert. Also fixing the precedence for printing "by" clause.
* Moving Refine to its proper module.Gravatar Pierre-Marie Pédrot2016-03-20
|
* Code factorization of tactic "unfold_body".Gravatar Pierre-Marie Pédrot2016-02-15
|
* More conversion functions in the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
|
* Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Moving is_quantified_hypothesis to new proof engine.Gravatar Hugo Herbelin2016-01-14
| |
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* | | Moving apply_type to new proof engine.Gravatar Hugo Herbelin2015-12-30
| | | | | | | | | | | | | | | | | | Note that code depending on apply_type might now have to ensure that typing constraints that were possibly generated by apply_type are now taken into account in advance.
* | | Moving specialize to Proofview.tactic.Gravatar Hugo Herbelin2015-12-25
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
| * Add tactic native_cast_no_check, analog to vm_cast_no_check.Gravatar Maxime Dénès2015-12-11
| |
* | Removing redundant versions of generalize.Gravatar Hugo Herbelin2015-12-05
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-03
|\|
| * Dead code from August 2014 in apply in.Gravatar Hugo Herbelin2015-12-02
| |
* | Monotonizing Tactics.change_arg.Gravatar Pierre-Marie Pédrot2015-10-29
| |
* | Type delayed_open_constr is now monotonic.Gravatar Pierre-Marie Pédrot2015-10-19
| |
* | Constraining refine to monotonic functions.Gravatar Pierre-Marie Pédrot2015-10-18
|/
* Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedGravatar Hugo Herbelin2015-09-08
| | | | to behave like "specialize (H ...)" since 4/8/2008 (r11300, 7d515acbc5).
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
| | | | | | takes a variable substitution for matched variables in the (lhs) pattern, and uses the existing ist structure to pretype the rhs correcly, without having to deal with the volatile evars.
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
| | | | | | | | | | | | | | | - no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
|
* Simplifying code of functional induction.Gravatar Hugo Herbelin2014-11-22
|
* Writing intro_replacing in the new monad.Gravatar Pierre-Marie Pédrot2014-11-22
|
* Writing Tactics.keep in the new monad.Gravatar Pierre-Marie Pédrot2014-11-21
|
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
| | | | | right-hand side of a "change with": the rhs lives in the toplevel environment.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:29:34 +0000