aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/g_decl_mode.ml4
Commit message (Expand)AuthorAge
* 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