aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
* Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atGravatar Pierre-Marie Pédrot2013-12-22
* Notations can now accept dummy arguments. If ever a bound variable is notGravatar Pierre-Marie Pédrot2013-12-22
* Vernac classification: allow for commands which start proofs but must be sync...Gravatar Arnaud Spiwack2013-12-04
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* STM: fix for PG and "Proof term" lines.Gravatar gareuselesinge2013-11-05
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
* Adds a tactical once.Gravatar aspiwack2013-11-02
* Added the tactical "tac1 + tac2".Gravatar aspiwack2013-11-02
* Fixes parsing of all: followed by a typechecking/evaluation command.Gravatar aspiwack2013-11-02
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
* declaration_hooks use EphemeronGravatar gareuselesinge2013-10-18
* STM: add "Stm Wait" to wait for the slaves to complete their jobsGravatar gareuselesinge2013-10-10
* STM: new command "Stm PrintDag" to force printing the dag to /tmpGravatar gareuselesinge2013-10-07
* STM: better handle proof modesGravatar gareuselesinge2013-09-30
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
* stm: (initial) support for -coq-slavesGravatar gareuselesinge2013-08-08
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
* Granting bug #3098: adding priority to Existing Instances.Gravatar ppedrot2013-08-01
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* More dynamic argument scopesGravatar letouzey2013-07-17
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Removing useless tactic arguments, and using generic argumentsGravatar ppedrot2013-06-27
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* More comments in Genarg.Gravatar ppedrot2013-06-06
* Replacing lists by maps in matching interpretation.Gravatar ppedrot2013-06-05
* More functional implementation of locality_flag and program_modeGravatar gareuselesinge2013-04-15
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Useless use of hooks in VernacDefinition. In addition, this wasGravatar ppedrot2013-02-10
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Implemented a full-fledged equality on [constr_expr]. By the way,Gravatar ppedrot2012-12-14
* Change [Hints Resolve] to still accept constrs as argumentsGravatar msozeau2012-10-31