aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
| | | | | | | | Ideally, any component of the global state that is a function or any other unmarshallable data should be stocked as an ephemeron to make the state always marshallable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing uses of Evar.add in class-related functions.Gravatar ppedrot2013-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16852 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
| | | | | | | | | | | | | | | | | | | state out of one we were threading all the way along. This should be safer, as one cannot forego side effects accidentally by manipulating explicitly the [sigma] container. Still, this patch raised the issue of badly used evar maps. There is an ad-hoc workaround (i.e. a hack) in Rewrite to handle the fact it uses evar maps in an unorthodox way. Likewise, that mean we have to revert all contrib patches that added effect threading... There was also a dubious use of side effects in their toplevel handling, that duplicates them, leading to the need of a rather unsafe List.uniquize afterwards. It should be investigaged. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16850 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing potential evar leak in Rewrite, and removing dead code.Gravatar ppedrot2013-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16849 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing potential evar leak in Equality.Gravatar ppedrot2013-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16848 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Class_tactics between code and CAMLP4/5 declarations.Gravatar ppedrot2013-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made rewrite tactic strategies pure. They were using quite uglilyGravatar ppedrot2013-09-28
| | | | | | references. Now they carry around their state explicitly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opacifying the type of strategies.Gravatar ppedrot2013-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16805 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Rewrite into a code part and a CAMLP4-dependent one.Gravatar ppedrot2013-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
| | | | | | | | | | | | casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing unused code from Term_dnet.Gravatar ppedrot2013-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16784 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing some evar_maps manipulation. In particular, using a [map] insteadGravatar ppedrot2013-09-05
| | | | | | of a [fold] in [nf_*] normalizing functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some cleanup in AutoGravatar ppedrot2013-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16758 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing some lone List.assoc & List.mem in lib.Gravatar ppedrot2013-08-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Actually using the domain function for maps.Gravatar ppedrot2013-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16736 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
| | | | | | | | 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
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | | | 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
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | 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
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
| | | | | | | | | 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
* Small fix in IStream interface.Gravatar ppedrot2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16667 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #3062. Computation of the value of a fresh identifier wasGravatar ppedrot2013-08-04
| | | | | | 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
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleaning of printing coercion failures in Ltac interpretation.Gravatar ppedrot2013-08-04
| | | | | | 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
* Small fixes due to the arrival of OCaml 3.12.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16656 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing an association list by a map in globalizing environment.Gravatar ppedrot2013-08-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pre-create typeclass_instances and rewrite hintdb in AutoGravatar letouzey2013-07-17
| | | | | | | | | | | 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
* Continuing r16621 on injection intro-patterns:Gravatar herbelin2013-07-10
| | | | | | | | - 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
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
| | | | | | | | | | | | - 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
* Removing SortArgType.Gravatar ppedrot2013-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
| | | | | | | | | | 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
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
| | | | | | | | | | | | 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
* Removed the ad-hod handling of wit_tacticn.Gravatar ppedrot2013-07-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Using functors to reduce the boilerplate used in registeringGravatar ppedrot2013-06-30
| | | | | | 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
* 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
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 09:29:00 +0000