aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
| | | | | | | Functions from Termops were sometimes fully qualified, sometimes not in the same module. This commit makes their usage more uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
| | | | | | | | | | These functions are applied much more often without labels than with them (the alternate of adding the label wherever relevant changes 124 lines instead of 41). Moreover, this is more consistent with the Term module and there is no ambiguity in argument types. This commit goes towards elimination of occurrences of OCaml warning 6. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13468 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug in implementation of setoid rewriting under cases andGravatar msozeau2010-09-27
| | | | | | | abstractions (reported by Pierre Courtieu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13466 85f007b7-540e-0410-9357-904b9bb8a0f7
* Solving bug #2212 (unification under tuples now not allowed forGravatar herbelin2010-09-24
| | | | | | flexible types what seems a reasonable strategy). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
| | | | | | | governed in the latter case by a flag since (useful e.g. for setoid rewriting which otherwise loops as it is implemented). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13443 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
| | | | | | revert the catch of anomalies in reductionops.ml now (commit 13353)? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverting partial fix for #2335 committed by mistake in r13435. Sorry.Gravatar herbelin2010-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch solving the bug but leaving open design choicesGravatar herbelin2010-09-19
| | | | | | | The patch does not address the possible use of evars by get_symmetric_proof in unify_eqn. Someting has still to be done there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13435 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
| | | | | | | | | | both for interpreting ltac patterns and patterns of "change pat with term". In particular, in the current status, Goal evars needs mandatorily to have the hole_kind GoalEvar. If this is too complicated to enforce, we might eventually consider another approach to the question of interpreting patterns in general. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13428 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
| | | | | | | | | | | | | | user either gives all missing arguments not dependent in the concl or all missing arguments not *recursively* dependent in the concl (as introduced by commit 13367). In practice, this means that "apply f_equal with A" remains allowed even though the new, recursive, analysis detects that all arguments of f_equal are inferable, including the first type argument (which is inferable from the knowledge of the function). Sized the opportunity to better explain the behavior of clenv_dependent. Also made minor code simplification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
| | | | | | See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
| | | | | | | | | | - improving error message when a reference to unfold is not found - repairing anomaly when an evaluable reference exists at internalisation-time but not at run time, and similarly for an arbitrary term (but the latter is new from 8.3 because of the new use of retyping instead of understand for typing Ltac values) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13408 85f007b7-540e-0410-9357-904b9bb8a0f7
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
| | | | | | | | | | | | | | | (declare_constant_gen was not exported, leading to a lot of silly tests before calling those functions) and replaced them by declare_constant : ?internal:internal_flat -> ... declare_constant's default behaviour is the same as the old declare_constant. * fixed the default behaviour of inductive scheme failure during coq's compilation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved printing of Unfoldable constants in hints databases (usedGravatar herbelin2010-09-02
| | | | | | | user-level pr_constant instead of debugging-level pr_con + used ppnl and boxes instead of explicit fnl's so as not to disturb formatting). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13390 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export printing functions for extra arguments. Maybe there's a way toGravatar msozeau2010-08-03
| | | | | | | get them from the grammar entries? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13369 85f007b7-540e-0410-9357-904b9bb8a0f7
* Capitulation wrt "change pat with term": instead of solving theGravatar herbelin2010-07-30
| | | | | | | | | | | problem raised by taral on coq-club Goal forall X : Prop, X -> False -> False. intro. change (?t -> False) with (not t). we just fail with an error message of "mauvaise foi". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13360 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2209, don't use the fragile argument name "y" to pass theGravatar msozeau2010-07-28
| | | | | | | missing argument to a transitivity call. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13347 85f007b7-540e-0410-9357-904b9bb8a0f7
* oops. commited files I shouldn't have. reverting on r13341Gravatar barras2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13342 85f007b7-540e-0410-9357-904b9bb8a0f7
* ported r13340 to trunkGravatar barras2010-07-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13341 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2010-07-27
| | | | | | | | | - Document and fix [autounfold] - Fix warning about default Firstorder tactic object not being defined - Fix treatment of implicits in Program Lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding the destauto tactic, that reduces match by destructing matchedGravatar courtieu2010-07-22
| | | | | | | term. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13307 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix for bug #2350 was really too quick. Here is a version that works better.Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13294 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13293 85f007b7-540e-0410-9357-904b9bb8a0f7
* Be more clever when trying to find out the relation inGravatar msozeau2010-07-15
| | | | | | | | reflexivity/symmetry/transitivity, reabstracting arguments if necessary. Makes instances on [_ <> _] work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13283 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish adding out-of-the-box support for camlp4Gravatar letouzey2010-07-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | If you want to try, it should be now as simple as: make clean && ./configure -local -usecamlp4 && make For the moment, the default stays camlp5, hence ./configure -usecamlp5 and ./configure are equivalent. Thanks to a suggestion by N. Pouillard, the remaining incompatibilities are now handled via some token filtering in camlp4. See compat5*.mlp. Morally, these files should be named .ml4, but I prefer having them not in $(...ML4) variables, it might confuse the Makefile... The empty compat5*.ml are used to build empty .cmo for making camlp5 happy. For camlp4, - tools/compat5.cmo changes GEXTEND into EXTEND. Safe, always loaded - tools/compat5b.cmo changes EXTEND into EXTEND Gram. Interact badly with syntax such that VERNAC EXTEND, we only load it for a few files via camlp4deps TODO: check that my quick adaptation of camlp5-specific code in tactics/extratactics.ml4 is ok. It seems the code by Chung-Kil Hur is hiding information in the locations ?! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13274 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix generalize_eqs tactic to not consider defined variables as being ↵Gravatar msozeau2010-06-30
| | | | | | generalizable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13226 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
| | | | | | | | | | | | them. This was the cause of the failure of compilation of CyclicAxioms after "replace" starting supporting open constrs (r13206). Seized the opportunity to clean a little bit things around nf_evar, whd_evar, check_evars, etc. Removed obsolete printer mod_self_id from dev/db. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13214 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made "replace" accepts open terms on its left-hand-side.Gravatar herbelin2010-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug introduced in a combination in r12807 and revealed inGravatar herbelin2010-06-28
| | | | | | r13080 via a failure in CoRN (pattern_of_constr needs correct sigma). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
| | | | | | | | | | checking function was used instead of a test of existence in the context. Also restricted constr_of_id which had no reason to interpret a posteriori an already interpreted identifier as a global reference. Consequently adapted funind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
| | | | | | | | By the way, there is an open problem of which conversion to use (conv, evarconv, with or w/o universes levels) when trying to unify multiple instances of the same variable in ltac pattern-matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
| | | | | | enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made intros_until and onInductionArg a bit stricter and robustGravatar herbelin2010-06-13
| | | | | | | | | | | | | The tolerance for overloading "id" as quantified hypothesis and as declared variable is kept - because induction_arg entry is not available to extended tactics, e.g. "discriminate", and these extensions do not know a priori if a name is quantified or declared. However, an upstream check is done to ensure that an induction argument exists as term if not quantified so that the tactics do not have to check this individually by themselves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
| | | | | | | swap in the evar flags and the isrec flag. (e.g. "induction" was printed "edestruct"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
| | | | | | | | | | | - made the example work (a call to whd_meta was missing) - replaced the internal error messages of w_unify_to_subterm_list into user-understandable messages - incidentally fixed the meaning of whd_meta (which now takes an evd) and meta_name (which now does what it means and do not treat differently the instantiated metas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
| | | | | | | | | | generalize the interface of Clenv to be able to use the existing treatment of bindings. Clenv functions did not use goals conclusions but insisted on getting goals anyway (which is even more problematic as goals appear in evar maps now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13102 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relaxed the freshness constraint in "intro H" (with "H" explicit):Gravatar herbelin2010-06-09
| | | | | | | don't forbid to overwrite a global reference of same basename. Should hopefully be more convenient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative fix for typeclass resolution raising Evd.define exceptions.Gravatar msozeau2010-06-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13087 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid computing tactic printing tree (std_ppcmds) when printing not needed inGravatar herbelin2010-06-03
| | | | | | eauto and class_tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13066 85f007b7-540e-0410-9357-904b9bb8a0f7
* New pass on inductive schemesGravatar herbelin2010-05-29
| | | | | | | | | | | | | | - Made "is defined" message quiet when a tactic define (via find_scheme) a scheme for internal use (in ind_tables.ml) - Improved documentation of eqschemes.ml (and swiched l2r/r2l terminology when talking about rewriting in hypotheses) - Took benefit of the new support for commutative cuts in the fixpoint guard checker for reducing the collection of rewriting schemes needed to implement the various kinds of rewriting (dependent or not, with symmetrical equality or not, in hypotheses or in conclusion, from left-to-right or from right-to-left) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Derive Inversion for new proof engineGravatar herbelin2010-05-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13027 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 16:02:52 +0000