aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-13- Inductive types in the "using" option of auto/eauto/firstorder areherbelin
interpreted as using the collection of their constructors as hints. - Add support for both "using" and "with" in "firstorder". Made the syntax of "using" compatible with the one of "auto" by separating lemmas by commas. Did not fully merge the syntax: auto accepts constr while firstorder accepts names (but are constr really useful?). - Added "Reserved Infix" as a specific shortcut of the corresponding "Reserved Notation". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12325 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
string in most commands expecting a global name (e.g. 'Print "+"' for an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly surrounded by a scope delimiter). Support for such smart globals in VERNAC EXTEND to do. Added a file smartlocate.ml for high-level globalization functions. Mini-nettoyage metasyntax.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-10Added syntax "exists bindings, ..., bindings" for iterated "exists".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12316 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Allow setoid rewrite to rewrite in pattern-matching scrutinees ormsozeau
branches when constructors have no arguments, requiring the output relation of the rewrite to be leibniz equality. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12314 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-09Stop trying to search if the relation is declared as a [RewriteRelation]msozeau
before attempting generalized rewriting as the relation may itself be instantiated during the unification of the lemma. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12312 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-03Support globality flag properly for "Add Morphism foo : foo_mor" syntax.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12306 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-02Stop unnecessary use of lazy values for constraints, simplifyingmsozeau
setoid_rewrite's code. Cleanup in vernacexpr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12303 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
only used to allow a module to be ended before the summaries were restored what can be solved by moving upwards the place where the summaries are restored). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12275 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
(uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06Move out JMeq of subst for compatibility (it affects e.g. theherbelin
compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq (maybe an option would be better??). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04- Add more precise error localisation when one of the application failsherbelin
in a chain of apply or apply-in. - Improved comments on the notions of permutation used in the library (still the equality relation in file Permutation.v misses the property of being effectively an equivalence relation, hence missing expected properties of this notion of permutation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04Fixed subst failing when a truly heterogeneous JMeq hyp is in theherbelin
context (problem introduced in r12259) + improved backward compatibility in hippatern.mli (wrt r12259). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12260 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-03Added "etransitivity".herbelin
Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Improved parameterization of Coq:herbelin
- add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Fixed a typo in "info" for tactic "right".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12257 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
I wonder how many of us were aware of the existence of such syntax ;-) Anyway, it is now subsumed by "rewrite by". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12248 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
unification for exact hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12239 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
more often but respects the spec better. The changes in the stdlib are reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing conversion with delta on open terms in that case). Also fix a minor bug in typeclasses not seeing typeclass evars when their type was a (defined) evar itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Simplify addition of hints to a hint_db. Rebuild the dnet associatedmsozeau
with it when the transparent state changes and not only when [Hint Unfold] is added. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12231 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
agreement with wish #2117 (pattern unification of evars remained deactivated for 3 years because of incompatibilities with eauto [see commit 9234]; thanks to unification flags, it can be activated for apply w/o changing eauto). Also add test for bug #2123 (see commit 12228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
traînaient un peu partout dans le code depuis la fusion d'evar_map et evar_defs. Début du travail d'uniformisation des noms donnés aux evar_defs à travers le code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
selection of occurrences. We use a new function [unify_to_subterm_all] to return all occurrences of a lemma and produce the rewrite depending on a new [conditions] option that controls if we must rewrite one or all occurrences and if the side conditions should be solved or not for a single rewrite to be successful. [rewrite*] will rewrite the first occurrence whose side-conditions are solved while [autorewrite*] will rewrite all occurrences whose side-conditions are solved. Not supported by [setoid_rewrite] yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-28Raise an error and not an anomaly if a rewrite is attempted on amsozeau
dependent argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12215 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-22Correct treatment of dependent products in signatures: create the evarsmsozeau
in the right environment and substitute the actual argument in the remaining signature. It works as long as we do no try to rewrite a dependent argument itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12207 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
necessary information. Fix implementation of [split_evars] and use splitting more wisely as it has a big performance impact. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12196 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-16Reimplementation of leibniz rewrite to control the instantiation of themsozeau
rewriting lemma more precisely. This should make rewrite properly fail when existentials are around instead of giving an identical goal up to new evars. Also a first step towards adding occurences to the leibniz rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12192 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
unnecessarily computed when the user won't see it (avoids the costly nf_evar_defs in typeclass errors). Add hook support for mutual definitions in Program. Try to solve only the argument typeclasses when calling [refine]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12185 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-11When typing a non-dependent arrow, do not put the (anonymous) variablemsozeau
in the context to avoid it being abstracted over in potential evars occuring in the codomain, which can prevent unifications. Add [intro] to the typeclasses eauto and fix [make_resolve_hyp] to properly normalize types w.r.t. evars before searching for a class in an hypothesis. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12182 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-10Use the projections for reflexivity, symmetry and transitivity proofs tomsozeau
ensure the type and relation used in the subgoals stay syntactically the same, for compatibility with [ring] which does not use conversion to find the ring on a relation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12179 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-09Correct handling of the initial existentials from the goal and the onesmsozeau
coming from the lemma in setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12178 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-08Do a fixpoint on the result of typeclass search to force themsozeau
resolution of generated evars, not doing any backtracking yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12175 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
- "*" implements Arthur Charguéraud's "introv" - "**" works as "; intros" (see also "*" in ssreflect). - Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui. - Shy attempt to seize the opportunity to clean Zarith_dec but Coq's library is really going anarchically (see a summary of the various formulations of total order, dichotomy of order and decidability of equality and in stdlib-project.tex in branch V8revised-theories). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12171 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-06Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0herbelin
instead of the index required by the user; extended FixRule and Cofix accordingly). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12168 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-01## Lines starting with '## ' will be removed from the log message.msozeau
## File(s) to commit: ## tactics/refine.ml Try solving typeclasses before refining in Refine.refine (suggested by S. Lescuyer). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12157 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
(bug 2092 and decl_mode.v in test suite). - Added a debugging printer for pftreestate. - Fixing American spelling in RefMan-decl.tex. - Optimizing application of tactic validation by removing consistency test in descend. - Fixing printing ambiguity for Hint Rewrite ->/<- in extratactics.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12134 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-18Minor unification changes:msozeau
- Primitive setup for firing typeclass resolution on-demand: add a flag to control resolution of remaining evars (e.g. typeclasses) during unification. - Prevent canonical projection resolution when no delta is allowed during unification (fixes incompatibility found in ssreflect). - Correctly check types when the head is an evar _or_ a meta in w_unify. Move [isEvar_or_Meta] to kernel/term.ml, it's used in two places now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12131 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-17- Allowing multiple calls to tactic fix with automatic generation ofherbelin
function name (instead of failure). - Making descent through conjunctions in apply work on recursive tuples such as Acc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12129 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-16Minor fixes in typeclasses:msozeau
- Set implicit args on for Context decls - Move class_apply tactic to Init - Normalize evars before raising an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-10- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itherbelin
revealed a too strict test for detection of inferable metas in Clenv. Restored tolerance for unbound names in interactive tactic use. - Moral removals of some captures of Not_found in Environ.evaluable_* since kernel is assumed to deal with existing names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
as hints (see wish #2104). - New type hint_entry for interpreted hint. - Better centralization of functions dealing with evaluable_global_reference. - Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had uglily to be factorized by hand. - Typography in RefMan-tac.tex. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-05-05Improvements in typeclasses eauto and generalized rewriting:msozeau
- Decorate proof search with depth/subgoal number information - Add a tactic [autoapply foo using hints] to call the resolution tactic with the [transparent_state] associated with a hint db, giving better control over unfolding. - Fix a bug in the Lambda case in the new rewrite - More work on the [Proper] and [subrelation] hints to cut the search space while retaining completeness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12118 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-28Fixes for bugs in r12110:msozeau
- [matches] is not parameterized by evars: normalize before calling conclPattern. - fix hints in Morphisms for subrelation and handling of signature normalization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12115 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27Cleanup old eauto code.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12111 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Implementation of a new typeclasses eauto procedure based on successmsozeau
and failure continuations, allowing to do safe cuts correctly. - Fix bug #2097 by suppressing useless nf_evars calls. - Improve the proof search strategy used by rewrite for subrelations and fix some hints. Up to 20% speed improvement in setoid-intensive files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12110 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Fixed a little bug in previous commit (bad failure in case of unknown entry).herbelin
- Added support for list of intropattern in Tactic Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12109 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
reorganization of code) and documentation (in pcoq.mli) of the code for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic Notation, Notation); merged the two copies of interp_entry_name to avoid they diverge. - Added support in Tactic Notation for ne_..._list_sep in general and for (ne_)ident_list(_sep) in particular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12108 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
clause resulting in stray notations for e.g. variable named "le") and 12083 (fixing bug in as clause of apply in) from trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12103 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
the interpretation mechanism of ltac variables) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12100 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-11 21:51:46 +0000