aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fixing Camlp4 compilation.Gravatar ppedrot2013-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16613 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed the distinction between generic Ltac vars and Let/IntroGravatar ppedrot2013-06-27
| | | | | | | | | | | | 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
* Added a generic handler of Ltac quotations, based on the existingGravatar ppedrot2013-06-27
| | | | | | | | | | | 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
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16610 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless tactic arguments, and using generic argumentsGravatar ppedrot2013-06-27
| | | | | | 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
* Bugfix: Fixing #3050Gravatar ppedrot2013-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Useless use of maps in constr internalizing.Gravatar ppedrot2013-06-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning up the type of Tacinterp.extract_ltac_constr_values.Gravatar ppedrot2013-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16606 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
| | | | | | | | 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
* Fixing the semantics of the previous patch.Gravatar ppedrot2013-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16603 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
| | | | | | of tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
| | | | | | | | | | | | | 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
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
| | | | | | | 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
* Revert "KEYID token makes parsing more robust in face of notations"Gravatar gareuselesinge2013-06-21
| | | | | | This reverts commit 950086cd26f83aa8896dde9dc7ef5b3d87307c56. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16599 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "parse "of" as KEYID "of""Gravatar gareuselesinge2013-06-21
| | | | | | This reverts commit edb2c43e152d40001616485fcf7fdde5d947f7a2. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16598 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving wit_unit to Stdarg.Gravatar ppedrot2013-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding genarg printer to debugger.Gravatar ppedrot2013-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing argument extension. Instead of qualified names, stringGravatar ppedrot2013-06-19
| | | | | | | 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
* - Keep the refinement of existing evars comming from unification with a ↵Gravatar msozeau2013-06-19
| | | | | | | | | | 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
* parse "of" as KEYID "of"Gravatar gareuselesinge2013-06-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16591 85f007b7-540e-0410-9357-904b9bb8a0f7
* KEYID token makes parsing more robust in face of notationsGravatar gareuselesinge2013-06-19
| | | | | | | | | 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
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
| | | | | | | | | | 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
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
| | | | | | 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
* Implementing a new interface for Genarg, with centralized dataGravatar ppedrot2013-06-18
| | | | | | | | 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
* Now glob_sign and interp_sign only depend on structures definedGravatar ppedrot2013-06-18
| | | | | | | 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
* Documenting a potential source of incompleteness in the ring tactic,Gravatar amahboub2013-06-17
| | | | | | | | 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
* Exporting field f_debug (needed for Ssreflect).Gravatar ppedrot2013-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using an "extra" Store.t field in interp_sign instead of dedicatedGravatar ppedrot2013-06-14
| | | | | | record fields. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16580 85f007b7-540e-0410-9357-904b9bb8a0f7
* When doing setoid_rewrite through rewrite, do resolution of classesGravatar msozeau2013-06-14
| | | | | | | 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
* Normalizing exception raised by tactic coercions.Gravatar ppedrot2013-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving coercion functions out of Tacinterp.Gravatar ppedrot2013-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Totally replaced ad-hoc tactic values by generic arguments. NowGravatar ppedrot2013-06-12
| | | | | | | 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
* Added Genarg as generic argument type.Gravatar ppedrot2013-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changing the type of Ltac values. Now they are toplevel genericGravatar ppedrot2013-06-12
| | | | | | | | | 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
* Fixing a Not_found and evar not found anomaly found in ATBR,Gravatar msozeau2013-06-12
| | | | | | | | 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
* One more fix for rewrite: disallow resolving of the (partial) constraintsGravatar msozeau2013-06-12
| | | | | | | | 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
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [setoid_rewrite] forgetting some evars that are produced when ↵Gravatar msozeau2013-06-10
| | | | | | | | | 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
* Cleanup in rewrite.ml4, remove Evd.merge... replaced by an evars_reset_evd Gravatar msozeau2013-06-07
| | | | | | | | (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
* Fixing bug #3030.Gravatar ppedrot2013-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3056Gravatar ppedrot2013-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16566 85f007b7-540e-0410-9357-904b9bb8a0f7
* More comments in Genarg.Gravatar ppedrot2013-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
| | | | | | | | | | | | | | | | | | 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
* Document changes and add missing documentation for Program options.Gravatar msozeau2013-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16563 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add an option to shrink the context of program obligations to avoidGravatar msozeau2013-06-06
| | | | | | | | 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
* Replacing lists by maps in matching interpretation.Gravatar ppedrot2013-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use a Summary.ref for the tactic in tactic options for proper backtrackingGravatar msozeau2013-06-05
| | | | | | | and handling of locality (fixes FingerTree contrib). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack on unneeded change of interface for pose_metas_as_evars.Gravatar msozeau2013-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
| | | | | | | | | according to a given strategy. - Enhance the hints/lemmas strategy to support "using tac" comming from rewrite hints to solve side-conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 08:36:54 +0000