aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/g_decl_mode.ml4
Commit message (Expand)AuthorAge
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* Getting rid of goal-dependency in declarative mode argument evaluation.Gravatar Pierre-Marie Pédrot2013-11-27
* Adds a new goal selector "all:".Gravatar aspiwack2013-11-02
* Cleanup of comments.Gravatar aspiwack2013-11-02
* STM: better handle proof modesGravatar gareuselesinge2013-09-30
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Revert "parse "of" as KEYID "of""Gravatar gareuselesinge2013-06-21
* parse "of" as KEYID "of"Gravatar gareuselesinge2013-06-19
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* No reason a priori for using unfiltered env for printingGravatar herbelin2013-01-29
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* 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
* Updating headers.Gravatar herbelin2012-08-08
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Corrects a (very) longstanding bug of tactics. As is were, tactic expectingGravatar aspiwack2012-04-18
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Noise for nothingGravatar pboutill2012-03-02
* Moving bullets (-, +, *) into stand-alone commands instead of beingGravatar courtieu2011-12-16
* Revert "Check if recursive calls are guarded before printing "Proof completed"."Gravatar pboutill2011-06-10
* Check if recursive calls are guarded before printing "Proof completed".Gravatar herbelin2011-05-26
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
* Fixed a bug causing inconsistent states during proof editting.Gravatar aspiwack2011-04-29
* Declarative mode: fix escape and return.Gravatar aspiwack2011-04-19
* Fixes the weird bug of the declarative proof mode (Czar) both in emacs and coqc.Gravatar aspiwack2011-04-06
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22