aboutsummaryrefslogtreecommitdiff
path: root/intf/vernacexpr.mli
AgeCommit message (Expand)Author
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2013-12-04Vernac classification: allow for commands which start proofs but must be sync...Arnaud Spiwack
2013-11-05STM: fix for PG and "Proof term" lines.gareuselesinge
2013-11-02Fixes parsing of all: followed by a typechecking/evaluation command.aspiwack
2013-11-02Adds a new goal selector "all:".aspiwack
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
2013-10-07STM: new command "Stm PrintDag" to force printing the dag to /tmpgareuselesinge
2013-09-30STM: better handle proof modesgareuselesinge
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08Support Proof Generalgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-01Added a Print Debug GC command that displays the current state ofppedrot
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
2013-07-17More dynamic argument scopesletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-06-06More comments in Genarg.ppedrot
2013-04-15More functional implementation of locality_flag and program_modegareuselesinge
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-11Allowing (Co)Fixpoint to be defined local and Let-style.ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-19Dir_path --> DirPathletouzey
2013-02-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
2012-12-18Modulification of nameppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
2012-10-29Fixed #2926:ppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-07-06A prototype implementation of a Print Namespace command.aspiwack
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Vernacexpr is now a mli-only file, locality stuff now in locality.mlletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 19:20:31 +0000