aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.mli
Commit message (Collapse)AuthorAge
* STM: fix for PG and "Proof term" lines.Gravatar gareuselesinge2013-11-05
| | | | | | | PG sends "Set Silent" and it was messing up the DAG, making the detection of an immediate proof not working. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17061 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
| | | | | | | | Exceptions raised during parsing are caught by the parser and result in weird parsing behaviour. Instead I added a special case in vernac_expr which always raises an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
| | | | | | all:tac applies tac to all the focused subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16982 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
| | | | | | | Used by fake_ide, that before editing a broken proof has to be sure Coq known the proof is broken. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16868 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16862 85f007b7-540e-0410-9357-904b9bb8a0f7
* STM: better handle proof modesGravatar gareuselesinge2013-09-30
| | | | | | | | Proof modes are really spaghetti code. It is a global state that you can't access (held by G_vernac). We stick it to the branches... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16820 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
* stm: (initial) support for -coq-slavesGravatar gareuselesinge2013-08-08
| | | | | | | Stm contains many TODO items to improve the thing, but it should be already possible to play with it (but not use it in production). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 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
* Support Proof GeneralGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16678 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
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
| | | | | | the OCaml GC, as indicated by [Gc.stat]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16651 85f007b7-540e-0410-9357-904b9bb8a0f7
* Granting bug #3098: adding priority to Existing Instances.Gravatar ppedrot2013-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16645 85f007b7-540e-0410-9357-904b9bb8a0f7
* More dynamic argument scopesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Register Inline command for the native compiler. Will be ported to ↵Gravatar mdenes2013-07-10
| | | | | | | | | | the VM too. Almost only a new grammar entry since the inlining machinery was already implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 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
* More functional implementation of locality_flag and program_modeGravatar gareuselesinge2013-04-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit introduces 2 new vernac_expr constructors: - VernacLocal (b,v) that represents a vernacular v with the "Local" modifier - VernacProgram v that represents a vernacular v with the "Program" modifier This allows the parser to avoid using side effects to model the two modifiers, that are now represented in the AST. This also decouples the parsing phase from the interpretation phase, since parsing a second phrase does not alter the locality flag for the first phrase. As a consequence all the locality_flag components of vernac_expr have been removed, but for the ones that (for retro compatibility) allow an "infix" Local flag. In these cases the boolean is renamed obsolete_locality (as the grammar entry that parses it), and during interpretation we check that at most one locality flag is specified, using the idiom (where the input local is the obsolete one): let local = enforce_XXX_locality locality local in Another improvement is that the default locality is not chosen in the parser, but in the interpreter where the idiom let local = make_XXX_locality locality in is used to default the locality to XXX (module/section/whatever). Unfortunately not all side effects have been removed: - Flags.program_mode is still used to signal that we are in program mode - Locality.LocalityFixme.* functions are used in commands that do not have an AST, but are parsed as VernacExtend (see vernacinterp.ml) I guess one could fix the latter case systematically adding an extra argument "locality" to commands attached using VERNAC COMMAND EXTEND. Fixing plugins adding commands that honour "Local" should look like this: VERNAC COMMAND EXTEND Set_Solver | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ set_default_tactic - (Locality.use_section_locality ()) + (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (Tacintern.glob_tactic t) ] END In any case the side effects are set/consumed within then interpretation phase, and not set during the parsing phase and consumed during the interpretation phase. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
| | | | | | | | | | | | After some investigation, I see no reason to try to hack the nametab in ppvernac, since everything happens there at a lower level (constr_expr). So the offending code that Enrico protected with a State.with_state_protection is now gone. By the way, moved some types from Declaremods to Vernacexpr to avoid some dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
| | | | | | | has to be refered through its qualified name even when the module containing it is imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dir_path --> DirPathGravatar letouzey2013-02-19
| | | | | | | | 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
* Useless use of hooks in VernacDefinition. In addition, this wasGravatar ppedrot2013-02-10
| | | | | | polluting the AST first-order structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16196 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of nameGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of dir_pathGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change [Hints Resolve] to still accept constrs as argumentsGravatar msozeau2012-10-31
| | | | | | | | to maintain compatibility, the term is then declared as a constant internally. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15948 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed #2926:Gravatar ppedrot2012-10-29
| | | | | | | Extend "Print Opaque Dependencies" for transparent dependencies as well git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
| | | | | | | | | | | | | instead of a general constr: this is the most common case and does not loose generality (one can simply define constrs before Hint Resolving them). Benefits: - Natural semantics for typeclasses, not class resolution needed at Hint Resolve time, meaning less trouble for users as well. - Ability to [Hint Remove] any hint so declared. - Simplifies the implementation as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
| | | | | | | | | | | | kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* A prototype implementation of a Print Namespace command.Gravatar aspiwack2012-07-06
| | | | | | | | | It is used as Print Namespace Coq.Init. This prototypes only prints the name of constants (hence no inductive types). The display order is a tad arbitrary too. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15537 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
| | | | | | | | | | | | | | | | | | | | | | Suppose we declare : Notation foo := bar (compat "8.3"). Then each time foo is used in a script : - By default nothing particular happens (for the moment) - But we could get a warning explaining that "foo is bar since coq > 8.3". For that, either use the command-line option -verb-compat-notations or the interactive command "Set Verbose Compat Notations". - There is also a strict mode, where foo is forbidden : the previous warning is now an error. For that, either use the command-line option -no-compat-notations or the interactive command "Unset Compat Notations". When Coq is launched in compatibility mode (via -compat 8.x), using a notation tagged "8.x" will never trigger a warning or error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vernacexpr is now a mli-only file, locality stuff now in locality.mlGravatar letouzey2012-05-29
Adds a directory ./intf for pure interfaces. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 03:50:30 +0000