| Commit message (Expand) | Author | Age |
* | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack | 2013-11-02 |
* | Future: better doc + restore ~pure optimization | gareuselesinge | 2013-10-31 |
* | Conv_orable made functional and part of pre_env | gareuselesinge | 2013-10-31 |
* | Do not generate useless argument arrays in whd_* functions. | ppedrot | 2013-10-29 |
* | Useless array to list conversions in proof/logic.ml. | ppedrot | 2013-10-28 |
* | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot | 2013-10-27 |
* | More monomorphic List.mem + List.assoc + ... | letouzey | 2013-10-24 |
* | cList: a few alternative to hashtbl-based uniquize, distinct, subset | letouzey | 2013-10-23 |
* | cList: set-as-list functions are now with an explicit comparison | letouzey | 2013-10-23 |
* | proof modes: use ephemerons to represent them in proof state | gareuselesinge | 2013-10-18 |
* | declaration_hooks use Ephemeron | gareuselesinge | 2013-10-18 |
* | Future: ported to Ephemeron + exception enhancing | gareuselesinge | 2013-10-18 |
* | Removing dubious use of evarmap manipulating functions in printing | ppedrot | 2013-10-05 |
* | Moving side effects into evar_map. There was no reason to keep another | ppedrot | 2013-10-05 |
* | Removing a bunch of generic equalities. | ppedrot | 2013-09-27 |
* | Removing useless evar-related stuff. | ppedrot | 2013-09-25 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot | 2013-09-18 |
* | Removing almost all new_untyped_evar, and a bunch of Evd.add. | ppedrot | 2013-09-18 |
* | Partly replacing list-based access functions in Evd. This is still | ppedrot | 2013-09-03 |
* | safe Conv_oracle state for type checking | gareuselesinge | 2013-08-30 |
* | Replacing lists by sets in clear tactic. | ppedrot | 2013-08-25 |
* | stm: (initial) support for -coq-slaves | gareuselesinge | 2013-08-08 |
* | get rid of closures in global/proof state | gareuselesinge | 2013-08-08 |
* | enhance marshallable option for freeze (minor TODO in safe_typing) | gareuselesinge | 2013-08-08 |
* | State Transaction Machine | gareuselesinge | 2013-08-08 |
* | Generalizing the use of maps instead of lists in the interpretation | ppedrot | 2013-06-22 |
* | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot | 2013-06-21 |
* | Fixing bug #3030. | ppedrot | 2013-06-06 |
* | Backtrack on unneeded change of interface for pose_metas_as_evars. | msozeau | 2013-06-04 |
* | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau | 2013-06-04 |
* | Removing a useless location in ltac trace mechanism. | ppedrot | 2013-05-30 |
* | Getting rid of LtacLocated exception transformer. | ppedrot | 2013-05-28 |
* | Use the Hook module here and there. | ppedrot | 2013-05-12 |
* | A uniformization step around understand_* and interp_* functions. | herbelin | 2013-05-09 |
* | Fixing ocamldoc compilation. | ppedrot | 2013-05-06 |
* | Removing a redundant function from Evd. | ppedrot | 2013-05-03 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | code simplifications concerning Summary | letouzey | 2013-04-22 |
* | Finer fix for bug 3017, mark unresolvability only of goals that are | msozeau | 2013-04-18 |
* | Fixing #2968. This is quite brittle though, because we are messing | ppedrot | 2013-04-16 |
* | Allow catching of WrongAbstractionType, fixing a regression from 8.4 | msozeau | 2013-04-05 |
* | Fix for bug #3017: wrong handling of the unresolvability status | msozeau | 2013-04-03 |
* | another Errors.push in a exception reraise | letouzey | 2013-03-16 |
* | Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical | letouzey | 2013-03-14 |
* | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey | 2013-03-13 |
* | Restrict (try...with...) to avoid catching critical exn (part 5) | letouzey | 2013-03-13 |
* | invalid_arg instead of raise (Invalid_argement ...) | letouzey | 2013-03-12 |
* | Allowing different types of, not to be mixed, generic Stores through | ppedrot | 2013-03-12 |