aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Split [Proofview] into a file where the basic operations on the state are ↵Gravatar Arnaud Spiwack2014-10-22
| | | | | | defined and the file providing the primitives. The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
* Make names in [Proofview_monad] more uniform.Gravatar Arnaud Spiwack2014-10-22
| | | | ret -> return, bind -> (>>=), etc… So that monads expose a [Monad.S] signature. Also Proofview now exposes the [Monad.S] signature directly rather than in a [Monad.S] subdirectory.
* Add more primitives to the [Monad.Make] arguments.Gravatar Arnaud Spiwack2014-10-22
| | | | For optimisation purposes.
* Proofview: move more functions to the Unsafe module.Gravatar Arnaud Spiwack2014-10-22
|
* 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.
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
| | | As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
* Remove duplicate code.Gravatar Arnaud Spiwack2014-10-22
|
* Removing dead code in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Small invariants in Rewrite code.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Fixing decompose_app_rel in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
| | | | | The old implementation did not beta-iota normalize before observing the head of the term, resulting in stange bugs.
* Using new clausenv in rewrite.Gravatar Pierre-Marie Pédrot2014-10-21
|
* Removing re-typecheking from "refine" in no-check mode of the newGravatar Hugo Herbelin2014-10-20
| | | | | | convert_concl/convert_hyp. This was actually probably the main source of inefficiency introduced on Oct 9 (see e.g. CoLoR), rather than nf_enter, as suspected in 3c2723f.
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une ↵Gravatar Hugo Herbelin2014-10-17
| | | | | | équation;" which was committed by mistake. This reverts commit a53b44aa042cfded28c34205074f194de7e2e4ee.
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
|
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
| | | | | | | | | | | | | | | | | | | | | | (continuation of 3087e0012eb12833a79b and 1f05decaea97f1dc). It may be the case that the new expression lives in a higher sorts and the context where it is substituted in supports it. So, it is too strong to expect that, when the substituted objects are types, the sort of the new one is smaller than the sort of the original one. Consider e.g. Goal @eq Type nat nat. change nat with (@id Type nat). which is a correct replacement, even if (id Type nat) is in a higher sort. Introducing typing in "contextually" would be a big change for a little numbers of uses, so we instead (hackily) recheck the whole term (even though typing with evars uses evar_conv which accept to unify Type with Set, leading to wrongly accept "Goal @eq Set nat nat. change nat with (@id Type nat).". Evar conv is however rejecting Prop=Type.)
* In convert_concl/convert_hyp: nf_enter -> enter.Gravatar Hugo Herbelin2014-10-16
| | | | (Maybe one of the source of inefficiency introduced on Oct 9 - see e.g. CoLoR.)
* Refresh to avoid algebraic universes on the right.Gravatar Matthieu Sozeau2014-10-16
|
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
| | | | The rest will take more work.
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
| | | | We are left with the compatibility layer and a handful of primitives which require some thought to move.
* 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.
* Fix for bug #3618.Gravatar Matthieu Sozeau2014-10-15
| | | | | Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars.
* Remaining tactics of the Auto module were put in the monad.Gravatar Pierre-Marie Pédrot2014-10-15
|
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
| | | | unification.
* Fixing "change" and "fold" after convert_hyp/convert_concl moved toGravatar Hugo Herbelin2014-10-13
| | | | | | | | | | | | | | new proof engine in e824d4293. Because of the expansion made by "fold" and possibly by "change", checking the order of hypotheses is necessary in general in "reduce". Before, it was done by side-effect on reference "check", now it has to be explicit. To do for optimization: flag each of the red_expr conversion strategy according to whether they really need a check. Also renamed the e_reduce family to e_change to emphasize that some expansion can occur and that typing has to be rechecked. This fixes recent failure of CoLoR (and probably Ergo).
* Add support for deactivating type class inference from induction/destruct.Gravatar Hugo Herbelin2014-10-13
|
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
| | | | Thanks to Yves for reporting it!
* Propagating name of goal to main subgoal in cut and conversion tactics.Gravatar Hugo Herbelin2014-10-09
|
* A version of convert_concl and convert_hyp in new proof engine.Gravatar Hugo Herbelin2014-10-09
| | | | | Not very optimized though (if we apply convert_hyp on any hyp, a new evar will be generated for every different hyp...).
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08
|
* 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.
* Removing debugging information committed by mistake.Gravatar Hugo Herbelin2014-10-07
|
* Make tclEFFECTS also update the env in the proof monadGravatar Enrico Tassi2014-10-06
|
* Semantic fix of a refine in Rewrite.Gravatar Pierre-Marie Pédrot2014-10-05
| | | | | This code was wrong but luckily unused. It instantiated an evar with an instance where the let-in bindings were removed.
* Check compatibility of types in change depending on whether it is aGravatar Hugo Herbelin2014-10-05
| | | | | | term or a type. Continuation of 9a82982c1eb.
* Fixing #3657 (check that both sides of a "change with" have the sameGravatar Hugo Herbelin2014-10-03
| | | | | type, what is necessary condition to ensure that the conversion of bodies will not raise an anomaly).
* Fixing bug #2810 (autounfold on local variable declared as hint but cleared).Gravatar Hugo Herbelin2014-10-02
|
* Fixing nice printing of error reporting with ml tactics bound to ltac names.Gravatar Hugo Herbelin2014-10-01
|
* Made Tacsubst independent of Auto at linking time so that Tacenv doesGravatar Hugo Herbelin2014-10-01
| | | | not draw Auto.
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
| | | | | | | | | | (the action is "clear"). Added subst_intropattern which was missing since the introduction of ApplyOn intro patterns. Still to do: make "intros _ ?id" working without interferences when "id" is precisely the internal name used for hypotheses to discard.
* 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.
* Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.Gravatar Matthieu Sozeau2014-09-27
|
* Make pattern_of_constr typed so that we can infer the proper patternsGravatar Matthieu Sozeau2014-09-27
| | | | | | for primitive projections, fixing bug #3661. Also fix expand_projection so that it does enough reduction to find the inductive type of its argument.
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* Changed semantics of induction !id when a clause is given: don'tGravatar Hugo Herbelin2014-09-27
| | | | authoritatively erase non-generalized hypotheses dependent on id.
* Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.Gravatar Pierre-Marie Pédrot2014-09-27
| | | | | | Most of the code from Goal.Refine and related was moved to the one file that was using it, wiz. tactics.ml. Some additional care should be taken to clean up even more the remaining code.
* Rename eq_constr functions in Evd to not break backward compatibilityGravatar Matthieu Sozeau2014-09-24
| | | | with existing ML code.
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
| | | | projections with their eta-expanded constant form.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 14:25:49 +0000