aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Collapse)Author
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
refine tactic, which now uses plain glob_constr's. Now there is no real need to depend on goal when interpreting genargs. Possible minor incompatibilities: 1. The interpretation of glob_constr to constr is now done by Goal.constr_of_raw, which may be slightly dumbier than the dedicated Tacinterp.interp_open_constr which tries harder. Stdlib and test-suite do go through, though. 2. I had to change the parsing level of wit_glob in Extraargs from lconstr to constr. It may break ML notations using glob, but as they are only used inside Coq code and all well-parenthezised, it should be OK.
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
parsing is plugged.
2013-11-25Tacinterp: fewer use of old-style goals.Arnaud Spiwack
There are many functions in Tacinterp which use a goal as a proxy for the pair of an environment and an evar_map. But do not build LCF tactics with them. They don't play well with the new style of tactics. I've changed some of them to explicitely take an environment and an evar_map instead.
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
Instead of putting the body directly in the AST, we register it in a table. This time it should work properly. Tactic notation are given kernel names to ensure the unicity of their contents. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-11-02Added the tactical "tac1 + tac2".aspiwack
It works pretty much like "tac1 || tac2" except that it has as successes all the successes of tac1 followed by all the successes of tac2 (whereas the latter has either the successes of tac1 (if there is at least one) or those of tac2 (otherwise)). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16998 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23CList.factorize_left with a parametric equalityletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16923 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-09Fixing CAMLP4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16865 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
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
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 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-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-30Fixing Camlp4 compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16613 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-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-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-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-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-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-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
In order to do so I had to move the data base of tactics to tacinterp (from tacintern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16540 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
exactly once at runtime, often to reduce the mutual dependency of modules. This module permits to track them more easily. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16509 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-17Fix some camlp5 quotations , restoring compatibility with camlp5 5.xletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16311 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Updated Exninfo to the new Store type.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-05More monomorphization.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Dir_path --> DirPathletouzey
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Added backtrace primitives.ppedrot
Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
It is supposed to become the next generation of the simpl tactics (it "refolds" constant) but 1/it is a bit more aggresive than the old simpl 2/it cannot be customized as simpl start to be 3/(for now)it does not refold in reccursive calls constant such as compare x y := compare_cont x y Eq := (fix compare_cont x y s := ...) x y Eq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16111 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of dir_pathppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Moving hcons_string to String namespace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16069 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
some cleaning of the interface and moving of code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Using library string functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16065 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13More monomorphizationsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13Added a CString module.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Added an Int module with dummy utility functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15956 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-12 11:13:46 +0000