aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Expand)AuthorAge
* safe Conv_oracle state for type checkingGravatar gareuselesinge2013-08-30
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* stm: (initial) support for -coq-slavesGravatar gareuselesinge2013-08-08
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Fixing bug #3030.Gravatar ppedrot2013-06-06
* Backtrack on unneeded change of interface for pose_metas_as_evars.Gravatar msozeau2013-06-04
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
* Removing a useless location in ltac trace mechanism.Gravatar ppedrot2013-05-30
* Getting rid of LtacLocated exception transformer.Gravatar ppedrot2013-05-28
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Fixing ocamldoc compilation.Gravatar ppedrot2013-05-06
* Removing a redundant function from Evd.Gravatar ppedrot2013-05-03
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Finer fix for bug 3017, mark unresolvability only of goals that areGravatar msozeau2013-04-18
* Fixing #2968. This is quite brittle though, because we are messingGravatar ppedrot2013-04-16
* Allow catching of WrongAbstractionType, fixing a regression from 8.4Gravatar msozeau2013-04-05
* Fix for bug #3017: wrong handling of the unresolvability statusGravatar msozeau2013-04-03
* another Errors.push in a exception reraiseGravatar letouzey2013-03-16
* Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalGravatar letouzey2013-03-14
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
* Removing Exc_located and using the new exception enrichementGravatar ppedrot2013-02-18
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Revised the Ltac trace mechanism so that trace breaking due toGravatar herbelin2013-02-17
* No reason a priori for using unfiltered env for printingGravatar herbelin2013-01-29
* Fixing bug #2969 (admit failing after Grab Existential Variables dueGravatar herbelin2013-01-29
* Fixed synchronicity of filter with evar context in new_goal_with.Gravatar herbelin2013-01-29
* Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envGravatar herbelin2013-01-29
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Added backtrace information to anomaliesGravatar ppedrot2013-01-28
* Reductionops: whd_state_gen can take and answers a cst_stack tooGravatar pboutill2013-01-24
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of nameGravatar ppedrot2012-12-18
* Fixed a little inefficiency of "set/destruct" over a pattern. NowGravatar herbelin2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* Monomorphization (proof)Gravatar ppedrot2012-11-25