aboutsummaryrefslogtreecommitdiff
path: root/plugins/decl_mode/g_decl_mode.ml4
AgeCommit message (Expand)Author
2017-03-07Farewell decl_modeEnrico Tassi
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-03Remove extraneous space in coqtop/pg output (bug #4675).Guillaume Melquiond
2016-03-19Moving the proof mode parsing management to Pcoq.Pierre-Marie Pédrot
2016-03-17Adding a universe argument to Pcoq.create_generic_entry.Pierre-Marie Pédrot
2016-03-17Removing the registering of default values for generic arguments.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-03-31Declarative mode: fix vernac classification.Arnaud Spiwack
2015-03-31Declarative mode: plug the specialised printers back.Arnaud Spiwack
2015-03-13rewiring Czar printers that were disabledPierre Corbineau
2015-03-11Fix double print in decl_mode.Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-05STM: new "par:" goal selector, like "all:" but in parallelEnrico Tassi
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2013-11-27Getting rid of goal-dependency in declarative mode argument evaluation.Pierre-Marie Pédrot
2013-11-02Adds a new goal selector "all:".aspiwack
2013-11-02Cleanup of comments.aspiwack
2013-09-30STM: better handle proof modesgareuselesinge
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-21Revert "parse "of" as KEYID "of""gareuselesinge
2013-06-19parse "of" as KEYID "of"gareuselesinge
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-01-29No reason a priori for using unfiltered env for printingherbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
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-08Updating headers.herbelin
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-04-18Corrects a (very) longstanding bug of tactics. As is were, tactic expectingaspiwack
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-02Noise for nothingpboutill
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:03:14 +0000