| Age | Commit message (Expand) | Author |
|---|
| 2013-10-28 | Useless array to list conversions in proof/logic.ml. | ppedrot |
| 2013-10-27 | Abstracting evar filter away. The API is not perfect, but better than nothing. | ppedrot |
| 2013-10-24 | More monomorphic List.mem + List.assoc + ... | letouzey |
| 2013-10-23 | 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-18 | 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-05 | 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-09-27 | Removing a bunch of generic equalities. | ppedrot |
| 2013-09-25 | Removing useless evar-related stuff. | ppedrot |
| 2013-09-19 | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc |
| 2013-09-18 | 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-03 | Partly replacing list-based access functions in Evd. This is still | ppedrot |
| 2013-08-30 | safe Conv_oracle state for type checking | gareuselesinge |
| 2013-08-25 | Replacing lists by sets in clear tactic. | ppedrot |
| 2013-08-08 | 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-06-22 | Generalizing the use of maps instead of lists in the interpretation | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-06 | Fixing bug #3030. | ppedrot |
| 2013-06-04 | 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-05-30 | Removing a useless location in ltac trace mechanism. | ppedrot |
| 2013-05-28 | Getting rid of LtacLocated exception transformer. | ppedrot |
| 2013-05-12 | Use the Hook module here and there. | ppedrot |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-05-06 | Fixing ocamldoc compilation. | ppedrot |
| 2013-05-03 | Removing a redundant function from Evd. | ppedrot |
| 2013-04-29 | Merging Context and Sign. | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 2013-04-18 | Finer fix for bug 3017, mark unresolvability only of goals that are | msozeau |
| 2013-04-16 | Fixing #2968. This is quite brittle though, because we are messing | ppedrot |
| 2013-04-05 | Allow catching of WrongAbstractionType, fixing a regression from 8.4 | msozeau |
| 2013-04-03 | Fix for bug #3017: wrong handling of the unresolvability status | msozeau |
| 2013-03-16 | another Errors.push in a exception reraise | letouzey |
| 2013-03-14 | Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical | letouzey |
| 2013-03-13 | 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-12 | invalid_arg instead of raise (Invalid_argement ...) | letouzey |
| 2013-03-12 | Allowing different types of, not to be mixed, generic Stores through | ppedrot |
| 2013-02-18 | Removing Exc_located and using the new exception enrichement | ppedrot |
| 2013-02-17 | Added propagation of evars unification failure reasons for better | herbelin |
| 2013-02-17 | Revised the Ltac trace mechanism so that trace breaking due to | herbelin |
| 2013-01-29 | No reason a priori for using unfiltered env for printing | herbelin |
