aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/extratactics.ml4
Commit message (Collapse)AuthorAge
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
| | | | | | Some asynchronous constraints between initial universes and the ones at the end of a proof were forgotten. Also add a message to print universes indicating if all the constraints are processed already or not.
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
| | | | | | | | | | | | | | | | Some functions from pretyping/typing.ml and their derivatives were potential source of evarmap leaks, as they dropped their resulting evarmap. This commit clarifies the situation by renaming them according to a unsafe_* scheme. Their sound variant is likewise renamed to their old name. The following renamings were made. - Typing.type_of -> unsafe_type_of - Typing.e_type_of -> type_of - A new e_type_of function that matches the e_ prefix policy - Tacmach.pf_type_of -> pf_unsafe_type_of - A new safe pf_type_of function. All uses of unsafe_* functions should be eventually eliminated.
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
|
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
| | | | | Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
* 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
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
|
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
| | | | | | | This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0. I had mixed up the boolean flag, resulting in the loss of evar-free versions of tactics.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
|
* Used an evar name based on the local def name in "evar" tactic.Gravatar Hugo Herbelin2014-11-25
|
* new: Optimize Proof, Optimize HeapGravatar Enrico Tassi2014-11-09
| | | | | | | | - drops all Defined entries from the evar map (applying the subst to the initial evar and the undefined evars types). - call Gc.compact Now the question is: where should these two commands be documented?
* Removing the legacy intro tactic code.Gravatar Pierre-Marie Pédrot2014-11-07
|
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
| | | | | | an updated evar_map, as pattern is working up to universe equalities that must be kept. Straightforward adaptation of the code depending on this.
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
| | | | The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
* Remove the deprecated open-constr based refine.Gravatar Arnaud Spiwack2014-10-22
| | | | | | | | That is [Tactics.New.refine]. Replaced it with a wrapper around the primitive refine [Proofview.Refine.refine], but with extra reductions on the resulting goals. There was two used of this refine: one in the declarative mode, and one in type classes. The porting of the latter is likely to have introduced bugs. Factored code with Ltac's refine in Extratactics.
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
| | | | | | Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine. The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
| | | | | | being able to export hints without tactics, vm, etc. to come with. Some functions moved to the new proof engine.
* Add syntax for naming new goals in refine: writing ?[id] instead of _Gravatar Hugo Herbelin2014-09-30
| | | | | | | | will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise.
* Merging some functions from evarutil.ml/evd.ml.Gravatar Hugo Herbelin2014-09-29
| | | | | | | | | | | | | - Removed collect_evars which does not consider instance (use evars_of_term instead). - Also removed evars_of_evar_info which did not filter context (use evars_of_filterered_evar_info instead). This is consistent with printing goal contexts in the filtered way. Anyway, as of today, afaics goals filters are trivial because (if I interpret evarutil.ml correctly), evars with non-trivial filter necessarily occur in a conv pb. Conversely, conv pbs being solved when tactics are called, there should not be an evar used as a goal with a non-trivial filter.
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | (but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on.
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
| | | | with existing ML code.
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
|
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
| | | | equality of universes, along with a few other functions in evd.
* Revert specific syntax for primitive projections, avoiding uglyGravatar Matthieu Sozeau2014-09-17
| | | | | | | | contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
* 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.
* Add a tactic [revgoals] to reverse the list of focused goals.Gravatar Arnaud Spiwack2014-09-08
|
* 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.
* 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].
* 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.
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
|
* 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.
* Add an is_cofix tacticGravatar Jason Gross2014-08-25
| | | | | | Should we also add is_* tactics for other things? is_rel, is_meta, is_sort, is_cast, is_prod, is_lambda, is_letin, is_app, is_const, is_ind, is_constructor, is_case, is_proj?
* Removing a use of Goal.refine.Gravatar Pierre-Marie Pédrot2014-08-19
|
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
| | | | Isolating a core tactic in replace, shareable to cutrewrite.
* 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)
* Better structure for Ltac pretyping environments.Gravatar Pierre-Marie Pédrot2014-08-07
|
* [uconstr]: use a closure instead of eager substitution.Gravatar Arnaud Spiwack2014-08-06
| | | | | This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine. As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
* 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).
* STM: new "par:" goal selector, like "all:" but in parallelGravatar Enrico Tassi2014-08-05
| | | | | par: distributes the goals among a number of workers given by -async-proofs-tac-j (defaults to 2).
* The [refine] tactic now accepts [uconstr].Gravatar Arnaud Spiwack2014-08-05
| | | Arguments of refine can hence be built by tactics instead of given in their entirety in one go.
* Add [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | | The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails. Together with [numgoal] can be used to fork on the number of goals of a tactic. The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
* Add a tactic [swap i j] to swap the position of goals [i] and [j].Gravatar Arnaud Spiwack2014-07-25
| | | If [i] or [j] is negative goals are counted from the end.
* Adds a cycle tactic to reorder goals in a loop.Gravatar Arnaud Spiwack2014-07-25
| | | [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1].
* 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.
* Oops, I fixed the .ml'sGravatar Matthieu Sozeau2014-06-23
|
* 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.
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
|
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
| | | | | | | | | | | | | corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib.
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-17 22:31:06 +0000