aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Collapse)AuthorAge
...
* 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.
* Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.Gravatar Pierre-Marie Pédrot2014-09-04
| | | | Hopefully, this may fix some nasty bugs lying around.
* Yes another remaining clearing bug with 'apply in'.Gravatar Hugo Herbelin2014-09-03
|
* Another fix than 19a7a5789c to avoid descend_in_conjunction to useGravatar Hugo Herbelin2014-09-02
| | | | | | | | | | | | | fresh names interferring with names later generated in intropatterns (as introduced in 72498d6d68ac which passed "clenv_refine_in continued by pattern introduction" to descend_in_conjunction while only a pure clenv_refine was passed before). The 72498d6d68ac version was generating fresh names in the wrong order (morally-private names for descend_in_conjunction before user-level names in clenv_refine_in). The 19a7a5789c fix was introducing expressions not handled by the refine from logic.ml. In particular, this fixes RelationAlgebra.
* Not using a "cut" in descend_in_conjunctions induced more success. WeGravatar Hugo Herbelin2014-08-29
| | | | | | at least remove the successes obtained by trivial unification of a meta with the goal, so as to avoid surprising results. We generalize this to variables which will only eventually be replaced by metas.
* Removing spurious tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-27
| | | | | | Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x] and we should try to reduce the use of this tactical, because it is mostly a legacy tactic.
* Fixing previous commit.Gravatar Pierre-Marie Pédrot2014-08-25
|
* Fixing a bug introduced in the extension of 'apply in' + simplifying code.Gravatar Hugo Herbelin2014-08-25
|
* Tactics.is_quantified_hypothesis does not reduce anymore to decide whetherGravatar Pierre-Marie Pédrot2014-08-23
| | | | | a variable is quantified in the goal. This is only used by induction, and it should be a bad practice to depend on an invisible binder.
* Tactics.unify in the new monad.Gravatar Pierre-Marie Pédrot2014-08-23
|
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
| | | | | | Some legacy code remains to keep the newish refine tactic working, but ultimately it should be removed. I did not manage to do it properly though, i.e. without breaking the test-suite furthermore.
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
| | | | | | | can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
| | | | Isolating a core tactic in replace, shareable to cutrewrite.
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
| | | | | scheme, redundancies, possibility of chaining a tactic knowing the name of introduced hypothesis, new proof engine).
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
| | | | | | | | | - made "apply" tactics of type Proofview.tactic, as well as other inner functions about elim and assert - used same hypothesis naming policy for intros and internal_cut (towards a reorganization of intro patterns) - "apply ... in H as pat" now supports any kind of introduction pattern (doc not changed)
* Fixing too restrictive detection of resolution of evars in "apply in"Gravatar Hugo Herbelin2014-08-16
| | | | (revealed by contribution PTSF).
* Restore the error-handling behavior of [change], which was silently failingGravatar Matthieu Sozeau2014-08-14
| | | | when conversion in the goal failed.
* In Hipattern: some functions not working modulo evar instantiation.Gravatar Arnaud Spiwack2014-08-07
| | | In theory [Proofview.Goal.env] should be, itself, marked as requiring a normalised goals (as it includes [hyps] which does). However, it is impractical as it is very common to pass a goal environment to a function reasoning modulo evars. So I guess we are bound to mark the appropriate functions by hand.
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | hypothesis when using it in apply or rewrite (prefix ">", undocumented), and a modifier to explicitly keep it in induction or destruct (prefix "!", reminiscent of non-linerarity). Also added undocumented option "Set Default Clearing Used Hypotheses" which makes apply and rewrite default to erasing the hypothesis they use (if ever their argument is indeed an hypothesis of the context).
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
| | | | subgoals and the role of the "by tac" clause swapped.
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
| | | | | | | | | | | | | obtained from case analysis or induction. Made it under experimental status. This replaces commit bf7d2a3ad2535e7d57db79c17c81aaf67d956965 which was acting at the level of logic.ml. Now acting in tactics.ml. Parts of things to be done about naming (not related to Propositions): induction on H:nat+bool produces hypotheses n and b but destruct on H produces a and b. This is because induction takes the dependent scheme whose names are statically inferred to be a and b while destruct dynamically builds a new scheme.
* Cleaning of the new implementation of the tactic monad.Gravatar Arnaud Spiwack2014-08-04
| | | | | | | | | * Add comments in the code (mostly imported from Monad.v) * Inline duplicated module * Clean up some artifacts due to the extracted code. * [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally) * Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code). * Remove Monad.v
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
| | | | catched otherwise due to the discrepancy between evars and metas.
* Restore proper order of effects in letin_tac_gen. Fixes CFGV again.Gravatar Matthieu Sozeau2014-07-03
|
* Synchronized names from the "as" clause with the skeleton of theGravatar Hugo Herbelin2014-06-30
| | | | | | elimination scheme in induction/destruct also for those names which correspond to neither the induction hypotheses nor the recursive arguments.
* Small refinement about whether it is tolerated for compatibility thatGravatar Hugo Herbelin2014-06-28
| | | | | | or-and intropatterns bind a limited number of patterns: if * or ** are used, the bound has to be used (since there is no heavy compatibility to respect for * and **). This fixes test-suite/success/intros.v.
* Moved code for finding subterms (pattern, induction, set, generalize, ...)Gravatar Hugo Herbelin2014-06-28
| | | | | | | into a specific new cleaned file find_subterm.ml. This makes things clearer but also solves some dependencies problem between Evd, Termops and Pretype_errors.
* Extra check for indirect dependency when abstracting a term which isGravatar Hugo Herbelin2014-06-28
| | | | | not a variable, in the future objective to factorize code between "generalize dependent" and "set", "destruct", etc.
* Made the subterm finding function make_abstraction independent of theGravatar Hugo Herbelin2014-06-28
| | | | proof engine. Moved it to unification.ml.
* Incorrect folding of evars in let_tac_gen made remember fail to storeGravatar Matthieu Sozeau2014-06-25
| | | | correct constraints (bug found in CFGV).
* In exact check, use e_type_of to ensure that universe constraints necessaryGravatar Matthieu Sozeau2014-06-25
| | | | | to typecheck the term are not forgotten. (relieves tactic implementors from calling e_type_of themselves, e.g. in congruence). Fixes a bug found in Containers.
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
| | | | | exhibits the "useless goal" behaviour: there is code out there depending on the fact that goals cannot be solved by side effects.
* Clenvtac.res_pf is in the new tactic monad.Gravatar Pierre-Marie Pédrot2014-06-24
|
* Removing opens to Clenvtac to track its use more easily.Gravatar Pierre-Marie Pédrot2014-06-23
|
* Fix semantics of change p with c to typecheck c at each specific occurrence ↵Gravatar Matthieu Sozeau2014-06-23
| | | | | | | of p, avoiding unwanted universe constraints in presence of universe polymorphic constants. Fixing HoTT bugs # 36, 54 and 113.
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
| | | | | | and avoiding explicit substitutions and merging of contexts, e.g. in obligations.ml. The context produced by typechecking a statement is passed in the proof, allowing the universe name context to be correctly folded as well. Mainly an API cleanup.
* Check resolution of Metas turned into Evars by pose_all_metas_as_evarsGravatar Hugo Herbelin2014-06-13
| | | | in unification.ml in case prefix 'e' of "apply" and co is not given.
* Passing some tactics to the new monad type.Gravatar Pierre-Marie Pédrot2014-06-12
|
* fix handling of side effects in abstract (fixes QArithSternBrocot)Gravatar Enrico Tassi2014-06-11
| | | | | The right fix should probably be to remove the build_constant_by_tactic function and only use the build_by_tactic one
* Preserve compatibility on examples such as "intros []." on goals suchGravatar Hugo Herbelin2014-06-06
| | | | | | | as "forall x:nat*nat, x=x", which resulted in "forall n n0 : nat, (n, n0) = (n, n0)" before commit 37f68259ab0a33c3b5b41de70b08422d9bcd3bec on "Fixing introduction patterns * and ** ".
* Collecting in Namegen those conventional default names that are used in ↵Gravatar Hugo Herbelin2014-06-04
| | | | different places
* Fixing introduction patterns * and ** when used in a branch so that they do ↵Gravatar Hugo Herbelin2014-05-31
| | | | not introduce beyond what is under control of the branch. See test-suite intros.v for an example.
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
|
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
| | | | | | | | | correctly when comparing stacks. - Disallow Type i <= Prop/Set constraints, that would otherwise allow constraints that make a universe lower than Prop. - Fix stm/lemmas that was pushing constraints to the global context, it is done depending on the constant/variable polymorphic status now. - Adapt generalized rewriting in Type code to these fixes.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 04:55:53 +0000