aboutsummaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
AgeCommit message (Expand)Author
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-25Removing useless try-with clauses in Goal.enter variants.Pierre-Marie Pédrot
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02Clean up a warning.aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-08-08State Transaction Machinegareuselesinge
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2011-11-14Bug 2636 - Move string_of_ppcmds to Pppboutill
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-26Moving implicit tactic support from Tacinterp to Pfedit and final evarherbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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-08Fixed "Scheme Equality" when another instance of the scheme on theherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-04- Add more precise error localisation when one of the application failsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 23:45:43 +0000