aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Better spec in Montgomery.ZBoundedGravatar Jason Gross2016-09-07
* Key on the head of the operation in reificationGravatar Jason Gross2016-09-07
* Add Common Subexpression EliminationGravatar Jason Gross2016-09-06
* Fix for 8.4's type inferencer being brokenGravatar Jason Gross2016-09-06
* Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refoldingGravatar Jason Gross2016-09-06
* Fix for 8.6 (context (correctly) no longer defaults to type_scope)Gravatar Jason Gross2016-09-06
* make 8.4 happierGravatar jadep2016-09-06
* Finished sqrt in GF25519Gravatar jadep2016-09-06
* Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...Gravatar jadep2016-09-06
* Add interp_flat_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Add correctness of interpretation of linearize and inline_constGravatar Jason Gross2016-09-05
* Add instances for interp_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Better implicits for interp_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Better implicits for interpf, pointwise-lifting of rels over interp_type_genGravatar Jason Gross2016-09-05
* Better implicits for interpfGravatar Jason Gross2016-09-05
* Better implicits for interpGravatar Jason Gross2016-09-05
* Better implicits for InterpGravatar Jason Gross2016-09-05
* Add LinearizeWfGravatar Jason Gross2016-09-05
* Reorder WfProofs argumentsGravatar Jason Gross2016-09-05
* Fix order of binders, and add WfProofsGravatar Jason Gross2016-09-05
* Better implicits for let_bind_constGravatar Jason Gross2016-09-05
* Better implicit arguments for under_letsfGravatar Jason Gross2016-09-05
* Better implicit arguments for linearizeGravatar Jason Gross2016-09-05
* Better implicit arguments for wf typesGravatar Jason Gross2016-09-05
* Merge pull request #60 from JasonGross/common-phoasGravatar Jason Gross2016-09-05
|\
| * Update comment with Andres' suggestionGravatar Jason Gross2016-09-05
| * More 8.4 fixesGravatar Jason Gross2016-09-05
| * Add comments to WfReflective, handle ExprGravatar Jason Gross2016-09-05
| * More 8.4 fixes (apparently rebinding [->] doesn't work)Gravatar Jason Gross2016-09-05
| * Fix _CoqProjectGravatar Jason Gross2016-09-05
| * Fix for 8.4 compatibilityGravatar Jason Gross2016-09-05
| * Remove ReifyDirectGravatar Jason Gross2016-09-05
| * A helper lemma for [Wf]Gravatar Jason Gross2016-09-05
| * PHOAS syntaxGravatar Jason Gross2016-09-05
|/
* Add nth_error_In from 8.6Gravatar Jason Gross2016-09-05
* Add connectives about option pointed_PropGravatar Jason Gross2016-09-05
* Add a coercion [bool >-> option pointed_Prop]Gravatar Jason Gross2016-09-05
* Fix a typoGravatar Jason Gross2016-09-05
* Add a file about pointed PropsGravatar Jason Gross2016-09-05
* Add a lemma about semidecidable things to DecidableGravatar Jason Gross2016-09-05
* Make [inversion_{prod,sigma}] strongerGravatar Jason Gross2016-09-05
* Transparent version of f_equal2Gravatar Jason Gross2016-09-05
* Reserve [->] like in 8.5, so we can redefine it in 8.4Gravatar Jason Gross2016-09-05
* Add path_prod_etaGravatar Jason Gross2016-09-03
* Make [inversion_option] work on Prop optionsGravatar Jason Gross2016-09-03
* Reserve λ notationGravatar Jason Gross2016-09-02
* Add reserved syntax-let notationGravatar Jason Gross2016-09-02
* Don't zeta-reduce in [simplify_projections]Gravatar Jason Gross2016-09-02
* Add prod_beqGravatar Jason Gross2016-09-02
* Strip <infomsg>; it messes things up in Coq 8.6 displayGravatar Jason Gross2016-09-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 03:42:23 +0000