aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| | | | printing functions touched in the kernel).
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
| | | | | One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem.
* Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Gravatar Matthieu Sozeau2015-01-16
| | | | | | Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73.
* Add a (by default deactivated) option to force typeclass resolution toGravatar Matthieu Sozeau2015-01-15
| | | | | respect dependencies between typeclass goals, trying to solve the least dependent ones first.
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
| | | | | | Off by default as it can be backwards-incompatible (e.g. produces loop in the library without an additional Typeclasses Opaque directive in RelationPairs).
* TCs: Properly handle Hint Extern with conclusions of the form _ -> _Gravatar Matthieu Sozeau2015-01-13
| | | | | in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fixing compilation of penultimate commit d08532d.Gravatar Hugo Herbelin2015-01-08
|
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
|
* Fix setoid rewrite.Gravatar Arnaud Spiwack2015-01-06
| | | Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false].
* Fixing #3896 (incorrect sigma given to printer).Gravatar Hugo Herbelin2015-01-03
|
* A global [gfail] tactic which works like [fail] except that it fails even if ↵Gravatar Arnaud Spiwack2014-12-23
| | | | | | there is no focused goal. The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
* Remove compatibility layer from Ltac's [fail].Gravatar Arnaud Spiwack2014-12-23
|
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
| | | | | | This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select". Fixes #3877.
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
| | | | [multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
| | | | | I added a emacs_logger. Still need to cleanup std_logger.
* Fixing bug #3796.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
|
* 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.
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
| | | | [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
| | | | You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
* In discrimination nets, do not index lambdas if they're part of a betaGravatar Matthieu Sozeau2014-12-12
| | | | redex.
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
| | | | pattern-matching predicate.
* Fix dummy argument use in guess_elim: there are some cases where X_indGravatar Matthieu Sozeau2014-12-10
| | | | is not defined while X_rect is, for example in HoTT/Coq.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Gravatar Hugo Herbelin2014-12-08
| | | | | | | As their commit messages suggested it, these commits were not intended to be committed at this time. They are part of a on-going merge of the code of induction and functional induction. Together with the fix here, they are supposingly transparent, semantically speaking.
* Constructor tactics backtracking is done using [Tacticals.New] rather than ↵Gravatar Arnaud Spiwack2014-12-08
| | | | | | | | | [Proofview]. The primitives in [Tacticals] respect Ltac's error level, whereas the one in [Proofview] do not necessarily. In that case the error caught was ignored causing arbitrary error level after [constructor] to be canceled. Needed the addition of an [ORD] variant to [OR] in [Tacticals.New] to avoid unnecessary precomputation (the 'D' stands for 'delay'). Fixes #3838.
* Step 4 : atomize_thenGravatar Hugo Herbelin2014-12-07
|
* Step 2Gravatar Hugo Herbelin2014-12-07
|
* Step 1Gravatar Hugo Herbelin2014-12-07
|
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
|
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
| | | | | | propagate it. This allows C-zar to continue to work. Don't know if it is the best way to do it.
* For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaGravatar Pierre-Marie Pédrot2014-12-02
| | | | normalize it afterwards.
* More invariants in the code of Rewrite.Gravatar Pierre-Marie Pédrot2014-12-01
| | | | | In particular, the old hypinfo is made as a proper cache, preventing dynamic tricks to decide whether it was rightful to refresh it.
* Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ↵Gravatar Hugo Herbelin2014-11-30
| | | | env.
* Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Gravatar Hugo Herbelin2014-11-30
| | | | This allows to have the example in test setoid_unif.v to work again.
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
| | | | | | | | | | | - Registering strict implicit arguments systematically (35fc7d728168) - Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6) - Fixing Coq compilation (894a3d16471) Systematically computing strict implicit arguments can lead to big computations, so I suspend this attempt, waiting for improved computation of implicit arguments, or alternative heuristics going toward having more conversion in rewrite.
* Experimenting always forcing convertibility on strict implicit argumentsGravatar Hugo Herbelin2014-11-26
| | | | in tactic unification.
* Used an evar name based on the local def name in "evar" tactic.Gravatar Hugo Herbelin2014-11-25
|
* One more word about "simpl f": avoid "simpl f" to be printed "simpl f",Gravatar Hugo Herbelin2014-11-23
| | | | at least when f is an evaluable reference.
* Partly revert commit d9681fb94a3e04a618e58cd09df9cee929170edc aboutGravatar Hugo Herbelin2014-11-23
| | | | | when the arguments of a constructor can be moved at the place of the variable on which destruct or induction applies.
* Specific printer of Evar.Set.t for ocamldebug + more information inGravatar Hugo Herbelin2014-11-22
| | | | a UserError to ease debugging.
* Attempt to organize and document unification flags of setoid rewrite.Gravatar Hugo Herbelin2014-11-22
|
* In setoid_rewrite error messages:Gravatar Hugo Herbelin2014-11-22
| | | | | | - removed the encapsulation in a Tactic Failure (I don't see why setoid_rewrite should specifically raise a Fail - do I miss something?) - avoid having twice a "Unable to satisfy ... constraints" message.
* Further simplifying functional induction.Gravatar Hugo Herbelin2014-11-22
|
* Simplifying code of functional induction.Gravatar Hugo Herbelin2014-11-22
|
* Not using an (arbitrary) pivot anymore for re-introduction ofGravatar Hugo Herbelin2014-11-22
| | | | | | | quantified hypothesis in functional induction. This has apparently no visible effect, probably because functional schemes do not have non-dependent hypothesis in their branches besides induction hypotheses which are anyway introduced at the top of the context.
* New simplification of code for generalizing hypotheses in destruct.Gravatar Hugo Herbelin2014-11-22
|
* Removing a hack which, according to the comment, should not be necessaryGravatar Hugo Herbelin2014-11-22
| | | | anymore since "destruct eq_dec" works like "destruct (eq_dec _ _)".
* Fix resolve_morphism to build well-scoped terms in case some argumentsGravatar Matthieu Sozeau2014-11-22
| | | | of the function are dependent.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:37:34 +0000