aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* 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
* 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 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
* Slightly better cfailGravatar Jason Gross2016-09-02
* Fix [ring] reference broken by moving [Require] outside a moduleGravatar Jason Gross2016-09-02
* Silence a warning about [Require] in 8.6Gravatar Jason Gross2016-09-02
* Add cfail{2,3}Gravatar Jason Gross2016-09-02
* Add [idtac_goal]Gravatar Jason Gross2016-09-02
* Add constr-based idtac tacticsGravatar Jason Gross2016-09-02
* Add another reserved notationGravatar Jason Gross2016-09-01
* Add more reserved infixesGravatar Jason Gross2016-08-31
* Add correctness theorems to Montgomery.ZBoundedGravatar Jason Gross2016-08-31
* Rename congrunce_option to inversion_option, add [inversion_prod]Gravatar Jason Gross2016-08-31
* Add congruence_option tacticGravatar Jason Gross2016-08-31
* updated GF25519 to match new exponentiation chain codeGravatar jadep2016-08-31
* Added square roots to GF1305, started reworking freeze_opt in preparation for...Gravatar jadep2016-08-31
* Generalized exponentiation chains so inverse and square roots can use the sam...Gravatar jadep2016-08-31
* Removed some commented-out code that will probably not be needed.Gravatar jadep2016-08-31
* Compatibility for 8.5; clear assumptions for an admitted canonicalization proof.Gravatar jadep2016-08-31
* Removed lingering SearchAbout.Gravatar jadep2016-08-31
* Proofs for MBS square roots.Gravatar jadep2016-08-31
* fixed typo; extra argumentGravatar jadep2016-08-31
* Parameterized square roots for primes that are 5 mod 8 over any computation o...Gravatar jadep2016-08-31
* Reworked square root theorems to prove they are valid iff a square root exist...Gravatar jadep2016-08-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 19:52:56 +0000