aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/functional_principles_proofs.ml
AgeCommit message (Expand)Author
2012-06-01More cleaningppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
2012-03-02Noise for nothingpboutill
2012-03-01New version of recdef :jforest
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
2011-05-13A new mechanism to handle errors.aspiwack
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-12-12Updated compatibility for rewriting equality proofs that are dependentherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-03Fixed small name freshness bug in Functional Scheme ("Heq" name washerbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey