| Commit message (Expand) | Author | Age |
* | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |
* | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau | 2013-06-04 |
* | Making the behavior of "injection ... as ..." more natural: | herbelin | 2013-06-02 |
* | Granting wish #3014: | ppedrot | 2013-05-12 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | code simplifications concerning Summary | letouzey | 2013-04-22 |
* | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey | 2013-03-13 |
* | Removing Exc_located and using the new exception enrichement | ppedrot | 2013-02-18 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau | 2012-12-08 |
* | Monomorphization (tactics) | ppedrot | 2012-11-25 |
* | Change Hint Resolve, Immediate to take a global reference as argument | msozeau | 2012-10-26 |
* | Continue killing hidden tactics : no more generated h_xxx | letouzey | 2012-10-15 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot | 2012-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Getting rid of Pp.msgnl and Pp.message. | ppedrot | 2012-06-01 |
* | tactic is_fix, akin to is_evar, is_hyp, is_ ... family | pboutill | 2012-05-31 |
* | Getting rid of Pp.msg | ppedrot | 2012-05-30 |
* | place all files specific to camlp4 syntax extensions in grammar/ | letouzey | 2012-05-29 |
* | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey | 2012-05-29 |
* | Glob_term now mli-only, operations now in Glob_ops | letouzey | 2012-05-29 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
* | Remove the Dp plugin. | gmelquio | 2012-04-17 |
* | Second step of integration of Program: | msozeau | 2012-03-14 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | A "Grab Existential Variables" to transform the unresolved evars at the end o... | aspiwack | 2012-02-07 |
* | Merge subinstances branch by me and Tom Prince. | msozeau | 2011-11-17 |
* | Add type annotations around all calls to Libobject.declare_object | letouzey | 2011-11-02 |
* | A new tactic is_var to check whether a term is a goal/section variable | letouzey | 2011-10-07 |
* | Moving implicit tactic support from Tacinterp to Pfedit and final evar | herbelin | 2011-09-26 |
* | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | 2011-06-18 |
* | - Fix treatment of globality flag for typeclass instance hints (they | msozeau | 2011-02-14 |
* | Rename the "raw" argument extension into "glob" | glondu | 2010-12-27 |
* | More {raw => glob} changes for consistency | glondu | 2010-12-24 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |
* | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
* | Add tactic has_evar (#2433) | glondu | 2010-12-02 |
* | Add tactic is_evar (Closes: #2433) | glondu | 2010-12-02 |
* | Delayed the evar normalization in error messages to the last minute | herbelin | 2010-11-07 |
* | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu | 2010-09-30 |
* | Remove some occurrences of "open Termops" | glondu | 2010-09-28 |
* | Some dead code removal, thanks to Oug analyzer | letouzey | 2010-09-24 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Adding the destauto tactic, that reduces match by destructing matched | courtieu | 2010-07-22 |