aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Collapse)Author
2013-07-10Added a Register Inline command for the native compiler. Will be ported to ↵mdenes
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
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-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-27Removing useless tactic arguments, and using generic argumentsppedrot
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
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-06More comments in Genarg.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16565 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16561 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
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
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
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
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16266 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
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
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-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
polluting the AST first-order structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16196 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-18Modulification of nameppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 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-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-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
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
2012-10-29Fixed #2926:ppedrot
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
2012-10-26Moved Entries module back to kernelppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15931 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
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
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15928 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
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15874 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06Tacexpr: revised version that doesn't need -rectypesletouzey
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
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
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
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02avoid referring to Term in constrexpr.mli and glob_term.mliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15842 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis ↵courtieu
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
2012-08-24Correcting a comment in pattern-matching compilation.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15758 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15731 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-07Avoid Pp.std_ppcmds in Misctypes.sort_infoletouzey
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
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
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
2012-07-06A prototype implementation of a Print Namespace command.aspiwack
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
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
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
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
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
2012-06-14Internalization of pattern is done in two phases.pboutill
First Notations, syntactic definitions, primitive entries are tackled to build raw_cases_pattern_expr. Reference are revolved at this time too. Then raw_patterns are internalized as cases_pattern or applied inductive (dealing with implicit args, or_pattern refactoring, aliases). It is more uniform, it allows notations for non fully applied constructors but : - It does not raise a warning when an identifier is also a global_reference different than a constructor. - It looks for implicit arguments twice. (because finding scopes of arguments asks for implicit arguments). - It does not deal anymore with constants that evaluates to constructor. (This one is voluntary, dealing with implicit & notations is already a hell full of bugs so what will be next step ? Any terms that computes to a pattern ???) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15439 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Extend become a mli-only file in intf/letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15390 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29No more Univ in grammar.cmaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in ↵letouzey
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Glob_term: minor formattingletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15379 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
NB: former Tacexpr.no_move is now Tacexpr.MoveLast (when introducing, intro with no move is intro as last) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 13:39:19 +0000