aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Collapse)Author
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
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
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.25.1) at 2026-04-24 14:57:35 +0000