aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* More invariants in Rewrite unification.Gravatar Pierre-Marie Pédrot2014-09-15
|
* The unifying functions of Rewrite uses the return types of strategies.Gravatar Pierre-Marie Pédrot2014-09-15
|
* Splitting the uses of the unification function according to the status ofGravatar Pierre-Marie Pédrot2014-09-15
| | | | the abs flag in rewrite.
* Rewrite.apply_strategy uses the same return type as strategies.Gravatar Pierre-Marie Pédrot2014-09-14
|
* Proper type for rewrite strategy results.Gravatar Pierre-Marie Pédrot2014-09-14
|
* Retroknowledge arguments are made VERNAC ARGUMENTS.Gravatar Pierre-Marie Pédrot2014-09-13
|
* Fixing injection bug #3616 on sigma-types.Gravatar Hugo Herbelin2014-09-13
|
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
|
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
| | | | | instances still to do). Using heuristics to name after the quantifier name it comes. Also added a "sigma" to almost all printing functions.
* Commit 682aa67cc80 about enforcing that apply does not create newGravatar Hugo Herbelin2014-09-12
| | | | | evars was too liberal. Using an intermediate criterion which makes both tests apply.v and 3284.v working.
* Oopps.. fixed the .ml not the .ml4Gravatar Matthieu Sozeau2014-09-11
|
* Use an AST for strategy names.Gravatar Matthieu Sozeau2014-09-11
|
* Add a flag for restricting resolution of typeclasses toGravatar Matthieu Sozeau2014-09-11
| | | | | | | matching (i.e. no instanciation of the goal evars). Classes defined when [Set Typeclasses Strict Resolution] is on use the restricted resolution for all their instances (except for Hint Extern's).
* Keeping a sub-optimal behavior of intros_possibly_replacing for ↵Gravatar Hugo Herbelin2014-09-11
| | | | compatibility with inversion
* Other bugs with "inversion as" (collision between user-provided names and ↵Gravatar Hugo Herbelin2014-09-11
| | | | generated equation names).
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
| | | | | | | | | | selection (rewrite, destruct/induction, set or apply on scheme), for unification (apply on not a scheme, auto), the latter being separated into primary unification and unification for merging instances. No change of semantics from within Coq, if I did not mistake (but a function like secondOrderAbstraction does not set flags by itself anymore).
* Fixing localisation of tactic errors (my mistake in himsg.ml essentially).Gravatar Hugo Herbelin2014-09-10
|
* More small bugs in intros_replacing.Gravatar Hugo Herbelin2014-09-10
|
* Fixing inversion after having fixed intros_replacingGravatar Hugo Herbelin2014-09-10
| | | | | | | in69665dd2480d364162933972de7ffa955eccab4d. There are still situations when "as" is not given where equations coming from injection are not yet removed, making invalid the computation of dependencies, what prevents an hypothesis to be cleared and replaced.
* Displaying genarg tag in idtac.Gravatar Pierre-Marie Pédrot2014-09-09
|
* Removing antiquotations in Tauto.Gravatar Pierre-Marie Pédrot2014-09-08
|
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
| | | | | Left a README, just in case someone will discover the remnants of it decades from now.
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
|
* Fix [induction] wrt inductive records and non-recursive variants.Gravatar Arnaud Spiwack2014-09-08
| | | | - [induction] on inductive records use the generated induction scheme for induction (not destruct as for non-recursive records) - [induction] on non-recursive variants do destruct as the induction scheme is not generated.
* Rename [extract_ltac_uconstr_values] to [extract_ltac_constr_context].Gravatar Arnaud Spiwack2014-09-08
| | | The latter is more representative of its actual function: extract from the Ltac context the values which are relevant to the interpretation of terms (either type or untyped).
* The [constr:(…)] Ltac construction now shares the same context as ↵Gravatar Arnaud Spiwack2014-09-08
| | | | | | [uconstr:(…)]. - The binders names can be influenced by binders defined in Ltac (e.g. [let x:=fresh"y" in let u:=constr:(fun x:nat=>x) in idtac u] ). - Any untyped constr in the context can now be inserted and type-checked inside a constr. In particular, Gregory Malecha's original proposed syntax for type-checking untyped terms in Ltac is now available [let u:=uconstr:(I I) in let v := constr:(u) in idtac v].
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
|
* A better check that an "as" clause has been given to inversion, soGravatar Hugo Herbelin2014-09-07
| | | | | | | that it clears things earlier in the "as" case, allowing intros_replacing to work without renaming the hypotheses. (clear_request was not a good idea here a priori, since its use was not related to the hypothesis to invert but to an hypothesis to inject).
* Fixing a bug in intros_replacing which was causing inversion notGravatar Hugo Herbelin2014-09-07
| | | | necessarily granting names given in the "as" clause.
* Fixing "simple inversion as" (bug #2164).Gravatar Hugo Herbelin2014-09-07
|
* Dead code in inv.ml.Gravatar Hugo Herbelin2014-09-07
|
* Inlining code in Tacinterp that was only used once.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Code simplification in Tacinterp.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Proper interpretation function for tauto.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | Instead of passing glob tactics through the infamous globTacticIn hack and antiquotation feature of the Ltac syntax, we put them in the interpretation environment as closures. This should be used everywhere to get rid of this buggy antiquotation syntax. This fixes bug #2800.
* Adding a way to inject tactic closures in interpretation values.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Fixing clearbody : typecheck definitions in context.Gravatar Pierre-Marie Pédrot2014-09-06
|
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
| | | | | | | | | | | 1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
* Retype terms resulting from the feeding of a context with a term.Gravatar Pierre-Marie Pédrot2014-09-05
| | | | Fixes bug #3455.
* Remove a redundant typing phase in the [refine] tactic.Gravatar Arnaud Spiwack2014-09-05
| | | The refined term is still typechecked twice (not counting Qed). But there seem to be a bug in the typechecker whereby it sometimes return terms which have universe inconsistencies. Until this is fixed, I'll leave the second typing phase which seems to catch these inconsistencies. To remove it, it suffices to change the [unsafe] flag to [true].
* Silence an ocaml warning.Gravatar Arnaud Spiwack2014-09-05
|
* Ltac's [uconstr] values now use the identifier context to give names to binders.Gravatar Arnaud Spiwack2014-09-05
| | | It does not work fine for refine yet as, while the binder has indeed the correct name, the evars are pretyped in an environment with the Ltac name, hence goal do not display the appropriate name.
* Adds an identifier context in pretying's Ltac context.Gravatar Arnaud Spiwack2014-09-05
| | | Binder names are interpreted as the Ltac specified one if available.
* Fix parsing of "subterm(s)" strategy argument.Gravatar Matthieu Sozeau2014-09-05
|
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
| | | | | | The code for the module was moved from Tacinterp. We still expose partially the implementation of the Ftactic.t type, for the sake of simplicity. It may be dangerous if used improperly though.
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-05
|
* At last a working clearbody!Gravatar Pierre-Marie Pédrot2014-09-05
| | | | | | | This time it should work at least as well as the previous version. The error messages were adapted a little. There is still a buggy behaviour when clearing lets in section, but this is mostly a problem of section handling. The v8.4 version of clearbody did exhibit the same behaviour anyway.
* Revert the two previous commits. I was testing in the wrong branch.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Removing the old implementation of clear_body.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Reimplementing the clearbody tactic.Gravatar Pierre-Marie Pédrot2014-09-04
|
* Proofview refiner is now type-safe by default.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | | | | | | In order not to be too costly, there is an [unsafe] flag to be set if the tactic does not have to check that the partial proof term is well-typed (to be used with caution though). This patch breaks one [fix]-based example in the refine test-suite, but a huge development like CompCert still goes through.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:29:02 +0000