aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Collapse)Author
2013-08-22Less "Coq" strings everywhereletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08get rid of closures in global/proof stategareuselesinge
In some cases, an 'a -> 'b field is changed into an ('a -> b') option field so that one can forget the closures and marshal the resulting state git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
The warning output by vernacextend when the classifier is missing is the documentation of this commit: Warning: Vernac entry "Foo" misses a classifier. A classifier is a function that returns an expression of type vernac_classification (see Vernacexpr). You can: - Use '... EXTEND Foo CLASSIFIED AS QUERY ...' if the new vernacular command does not alter the system state; - Use '... EXTEND Foo CLASSIFIED AS SIDEFF ...' if the new vernacular command alters the system state but not the parser nor it starts a proof or ends one; - Use '... EXTEND Foo CLASSIFIED BY f ...' to specify a global function f. The function f will be called passing "Foo" as the only argument; - Add a specific classifier in each clause using the syntax: '[...] => [ f ] -> [...]'. Specific classifiers have precedence over global classifiers. Only one classifier is called. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16680 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08State Transaction Machinegareuselesinge
The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
new Axiom in Logic.v, proof_admitted : False. admit now simply cases proof_admitted and does not create a new Axiom in the environment. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Small fix in IStream interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Fixing #3062. Computation of the value of a fresh identifier wasppedrot
done too early and lead to dynamic conflicts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16660 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Removing useless casts between arrays and lists.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
Now we at least print the type of the offending object. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16657 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16656 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-03Replacing an association list by a map in globalizing environment.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-17Pre-create typeclass_instances and rewrite hintdb in Autoletouzey
This way, we avoid relying on the add_auto_init hook. This hook is left for the moment, but could probably be removed someday. We also stop using create_hint_db, which has an effect on the libstack. This wasn't a problem per se, but could if init_summaries is used more (for instance to temporary reset coq). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16624 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-10Continuing r16621 on injection intro-patterns:herbelin
- order of hypothesis was (historically) from right to left in injection but already from left to right in decomp_eq, so no need ro fix it there - made test Injection.v consistent with implementation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16622 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
- Introduction of a specific notation for injection intropatterns: [= pats] - Use of this specific pattern also to apply discriminate on the fly Note: The automatic injection of dependent tuples over a same first component (introduced in r10180) still not integrated to the main parts of injection and its variant (indeed, it applies only for a root dependent tuple in sigT). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16621 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-05Removing SortArgType.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
level of generic arguments. This only matters at parsing time. TODO: the current status is not satisfactory enough, as rule emptyness is still decided w.r.t. generic arguments. This should be done on a grammar entry basis instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
through a unique generic argument, and the level is only considered at parsing time. This may introduce unnecessary parentheses in Ltac printing though, as every tactic argument is collapsed at the lowest level. I assume this does not matter that much, and anyway Ltac printing is quite bugged as of today. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-02Removed the ad-hod handling of wit_tacticn.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16615 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-30Using functors to reduce the boilerplate used in registeringppedrot
generic argument stuff, including the unsafe Obj.magic-like casts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16614 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
bindings, which permits using only one environment for interning terms. Ltac semantics was sligthly changed, as it required introducing a lot of additional coercions from goal variables to other types. Ltac seemed to be quite non-uniform, as it tried to represent hypotheses with intropatterns, instead of the dedicated var type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16612 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Getting rid of IntroPatternArgType.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Removing useless tactic arguments, and using generic argumentsppedrot
instead (proof of concept, to be extended). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16609 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-27Bugfix: Fixing #3050ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16608 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-25Useless use of maps in constr internalizing.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-24Cleaning up the type of Tacinterp.extract_ltac_constr_values.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16606 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-24Using the whole tactic environment while Pretyping.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-22Now, idtac closures use maps instead of association list.ppedrot
The semantics changed slightly so it may break some scripts, though it is very unlikely, as they would have to be quite intricated and poorly written. Indeed, the test-suite passed just fine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16604 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-22Fixing the semantics of the previous patch.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16603 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
of tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21Splitted up Genarg in four different levels:ppedrot
1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
related types. This will ultimately allow putting genargs into these ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-19Moving wit_unit to Stdarg.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-19- Keep the refinement of existing evars comming from unification with a ↵msozeau
rewrite lemma. - Do an nf_meta before get_type_of in unify_to_type to avoid a possible NotAnArity exception, raised by type_of_*_knowing_parameters. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16592 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
their own file, Stdarg. This required a little trick to correctly handle wit_* naming. We use a dynamic table to remember exactly where those arguments come from. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
extra argument types and putting them into Genarg. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-18Now glob_sign and interp_sign only depend on structures definedppedrot
upto Genarg, so moved them there. This will allow defining the new genarg interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-14Exporting field f_debug (needed for Ssreflect).ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16581 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-14Using an "extra" Store.t field in interp_sign instead of dedicatedppedrot
record fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16580 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-14When doing setoid_rewrite through rewrite, do resolution of classesmsozeau
in w_unify_to_subterm, deactivated by previous patch (fixes RelationAlgebra). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16579 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-13Normalizing exception raised by tactic coercions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16578 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Moving coercion functions out of Tacinterp.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16577 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Totally replaced ad-hoc tactic values by generic arguments. Nowppedrot
only tactics results are special tactic values represented by the non-exported tacvalue type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16576 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Added Genarg as generic argument type.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16575 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Changing the type of Ltac values. Now they are toplevel genericppedrot
arguments. That way we will be able to define interpretation of tactics without referring to tactic values. Quite ad-hoc for now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16574 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12Fixing a Not_found and evar not found anomaly found in ATBR,msozeau
related to setoid_rewrite t where t containts evars, to be added to the goal evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16573 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-12One more fix for rewrite: disallow resolving of the (partial) constraintsmsozeau
happening silently in w_unify and handle this explicitely. Class resolution filters now can test the existential key. Fixes Ergo contrib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16571 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-10Hiding tactic value representations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16570 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-10Fix [setoid_rewrite] forgetting some evars that are produced when ↵msozeau
typechecking a lemma to apply, fixes test-suite test. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16569 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-07Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd msozeau
(to push the metas from a clenv into the current evars). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16568 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 20:00:25 +0000