aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* 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
* Fixed #2926:Gravatar ppedrot2012-10-29
* Moved Entries module back to kernelGravatar ppedrot2012-10-26
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* Tacexpr: revised version that doesn't need -rectypesGravatar letouzey2012-10-06
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* avoid referring to Term in constrexpr.mli and glob_term.mliGravatar letouzey2012-10-02
* Added a new tactical infoH tac, that displays the names of hypothesis created...Gravatar courtieu2012-10-01
* Correcting a comment in pattern-matching compilation.Gravatar aspiwack2012-08-24
* Added support for option Local (at module level) in Tactic Notation.Gravatar herbelin2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07