aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-30Fixing Camlp4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16613 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-27Added a generic handler of Ltac quotations, based on the existingppedrot
syntax constr:foo and ipattern:bar (which is not very nice for parsing, b.t.w.). Now one is able to dynamically add quotations of the form name:... that will use the provided function to create a dynamically typed argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16611 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-21Revert "KEYID token makes parsing more robust in face of notations"gareuselesinge
This reverts commit 950086cd26f83aa8896dde9dc7ef5b3d87307c56. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16599 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-21Revert "parse "of" as KEYID "of""gareuselesinge
This reverts commit edb2c43e152d40001616485fcf7fdde5d947f7a2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16598 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-19Adding genarg printer to debugger.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16594 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-19Fixing argument extension. Instead of qualified names, stringppedrot
representing qualified names where interpreted as a whole lowercase ident. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16593 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-19parse "of" as KEYID "of"gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16591 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-19KEYID token makes parsing more robust in face of notationsgareuselesinge
A notation may introduce a new keyword that masks an quasi keyword (IDENT "of" for example) used in some grammar rules. KEYID "of" acepts both "of" as an ident and "of" as a keyword. Rephrasing grammar rules with KEYID makes hence them more robust in face of user notations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16590 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-18Implementing a new interface for Genarg, with centralized datappedrot
structure. The code is quite dumb for now, as it only handles basic extended generig arguments (ExtraArgTypes). Soon, code from other modules will be centralized there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16585 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-17Documenting a potential source of incompleteness in the ring tactic,amahboub
when reification is customized with a user-defined set of coefficients. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16583 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
2013-06-06Fixing bug #3030.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16567 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Fixing #3056ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16566 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06More comments in Genarg.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Uniformizing generic argument types.ppedrot
Now, instead of having three unrelated types describing a dynamic type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type" whose parameters describe the reified type at each level. This has various advantages: - No more code duplication to handle the three level separately; - Safer code: one is not authorized to mix unrelated types when what was morally expected was a genarg_type. - Each level-specialized representation can be accessed through well-typed projections: rawwit, glbwit and topwit. Documenting a bit Genarg b.t.w. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16564 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Document changes and add missing documentation for Program options.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-06Add an option to shrink the context of program obligations to avoidmsozeau
unnecessary dependencies (applies to obligations defined by tactics only). Satisfies RFE #1984. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16562 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-12 02:18:17 +0000