aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2012-01-31Fix camlp4 compilationpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2012-01-23Fix for Program Instance not separately checking the resolution of evars of t...msozeau
2012-01-23Another quick hack that works this time, to handle printing of locality in Pr...ppedrot
2012-01-20Reverted previous commit, which broke library compilation.ppedrot
2012-01-20This is a quick hack to permit the parsing of the locality flag in the Progra...ppedrot
2012-01-17Fixed the pretty-printing of the Program plugin.ppedrot
2012-01-14coq_micromega.ml: fix order of recursive calls to rconstantglondu
2012-01-14More newlines in debugging output of psatzlglondu
2012-01-13Added a Btauto plugin, that solves boolean tautologies.ppedrot
2012-01-12Fix typoglondu
2011-12-16Moving bullets (-, +, *) into stand-alone commands instead of beingcourtieu
2011-12-12Proof using ...gareuselesinge
2011-12-10Extraction: only do the test on generalizable lets for ocamlletouzey
2011-12-08Extraction: avoid internal eta-reduction (fix #2570)letouzey
2011-11-30Extraction: try to avoid issues with an Include directly inside a .vletouzey
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
2011-11-29Extraction: typo in last commitletouzey
2011-11-29fix for bug #2649corbinea
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-24Fixed some missing options from previous commit.ppedrot
2011-11-24Added a DEPRECATED flag in declaration of options. For now only two options a...ppedrot
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-28Remove dynamic stuff from constr_expr and glob_constrglondu
2011-10-27Remove avoidable use of GDynamicglondu
2011-10-22Fixing Equality.injectable which did not detect an equality withoutherbelin
2011-10-18Fix bug #2227msozeau
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-10-07Fix bug #2557 and an issue with Propers for complementmsozeau
2011-10-05Fixing Implicit Tactic mode damaged by commit r14496 (see also bug #2612).herbelin
2011-09-27In Coq_config: get rid of coqsrc and make coqlib optionalglondu
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Generalizing subst_term_occ so that it supports an arbitrary matchingherbelin
2011-09-23Fix commit 14489: missing Coq. in dirpathletouzey
2011-09-23Program: add some check_required_library (fix #2592) + some dead code removalletouzey
2011-09-16Omega: for non-arithmetical goals, try proving False from context (wish #2236)letouzey
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
2011-09-09correction du bug 2047jforest
2011-09-06Improved ltac code for zify (fix #2575).letouzey
2011-09-05Extraction Implicit: fix the numbering of constructor argumentsletouzey
2011-09-02Bug 2589: Documentation patch of Hendrik Tewspboutill
2011-08-25Extraction: allow extraction of records with anonymous fields (fix #2555)letouzey
2011-08-08New proposition "rewrite Heq in H" for eq_rect (assuming that there isherbelin
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-08-04moins de reification inutile, noatations standardspottier
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 09:21:02 +0000