aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_vernac.ml4
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2014-02-02Removing the [Require "file"] syntax.Pierre-Marie Pédrot
2014-01-13Documenting old but useful command "Print Tables".Hugo Herbelin
2014-01-10Fixing bug #3144.Pierre-Marie Pédrot
2013-12-12Patch for supporting [From Xxx Require Yyy Zzz.]Gregory Malecha
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-02Fixes parsing of all: followed by a typechecking/evaluation command.aspiwack
2013-11-02New option Default Goal Selector.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-08-19Modulification and removing of structural equality in Stateid.ppedrot
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-05-28Fixing warning of deprecated Argument Scopes.ppedrot
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
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-10Useless use of hooks in VernacDefinition. In addition, this wasppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-11-25Monomorphization (parsing)ppedrot
2012-10-29Fixed #2926:ppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-07-11Re-allow Reset in compiled filesletouzey
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-06-04Added a color output to Coqtop.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29Migrate the grammar entry about "Ltac" into g_vernac.ml4.letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
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
2012-04-26Program: avoid staying in program mode after a failed Program commandletouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-23Remove undocumented command "Delete foo"letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 03:22:36 +0000