aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Collapse)AuthorAge
* 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
* 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
* 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
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | | | | When refering to a module / module type, or when doing an include, we do not duplicate and substitution original libobjects immediatly. Instead, we store the module path, plus a substitution. The libobjects are retrieved later from this module path and substituted, typically during a Require. This allows to vastly decrease vo size (up to 50% on some files in the stdlib). More work is done during load (some substitutions), but the extra time overhead appears to be negligible. Beware: all subst_function operations should now be environment-insensitive, since they may be arbitrarily delayed. Apparently only subst_arguments_scope had to be adapted. A few more remarks: - Increased code factorisation between modules and modtypes - Many errors and anomaly are now assert - One hack : brutal access of inner parts of module types (cf handle_missing_substobjs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 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
* 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
* 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
* 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
* 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
* 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
* 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
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
| | | | | | | | | | | | | 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
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
| | | | | | | | | | | 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
* 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
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
| | | | | | 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
* 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
* Moved Entries module back to kernelGravatar ppedrot2012-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15931 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
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 85f007b7-540e-0410-9357-904b9bb8a0f7
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15896 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tacexpr: revised version that doesn't need -rectypesGravatar letouzey2012-10-06
| | | | | | | For that, gen_atomic_tactic_expr and gen_tactic_expr are now mutually recursive git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15866 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
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15842 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a new tactical infoH tac, that displays the names of hypothesis ↵Gravatar courtieu2012-10-01
| | | | | | created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correcting a comment in pattern-matching compilation.Gravatar aspiwack2012-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15758 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
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
| | | | | | | | Otherwise, after a Set Printing Universes we may end on a comparison of Pp.std_ppcmds, which may fail on functional values (cf. Constrextern.check_same_type), as notice by Pierre-Marie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15697 85f007b7-540e-0410-9357-904b9bb8a0f7
* The tactic remember now accepts a final eqn:H option (grant wish #2489)Gravatar letouzey2012-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
| | | | | | | | | | | | | | | | | | The ugly syntax "destruct x as [ ]_eqn:H" is replaced by: destruct x eqn:H destruct x as [ ] eqn:H Some with induction. Of course, the pattern behind "as" is arbitrary. For an anonymous version, H could be replaced by ?. The old syntax with "_eqn" still works for the moment, by triggers a warning. For making this new syntax work, we had to change the seldom-used "induction x y z using foo" into "induction x, y, z using foo". Now, only one "using" can be used per command instead of one per comma-separated group earlier, but I doubt this will bother anyone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 13:37:33 +0000