gmalecha/mirror-core issues and pull requests

#107 - Get mirror-core building with Coq 8.10

Pull Request - State: closed - Opened by JasonGross about 5 years ago - 1 comment

#106 - Compilation error Mirror-core 1.0.0 package, Coq 8.5.0

Issue - State: closed - Opened by clarus over 5 years ago - 5 comments

#105 - Fix broken links to Gregory's website

Pull Request - State: closed - Opened by bmsherman over 7 years ago

#104 - Coq 8.6 Support

Issue - State: open - Opened by gmalecha over 7 years ago
Labels: enhancement

#103 - Parsing patterns should do reduction to hnf.

Issue - State: open - Opened by gmalecha about 8 years ago
Labels: enhancement

#102 - Added a reifiction function for modular reification without pmaps.

Pull Request - State: open - Opened by jesper-bengtson about 8 years ago - 4 comments

#101 - report parse failures in the plugin

Pull Request - State: closed - Opened by gmalecha about 8 years ago - 1 comment
Labels: enhancement

#100 - Reify.v invalidates valid syntax

Issue - State: open - Opened by jesper-bengtson about 8 years ago - 1 comment

#99 - General cleanup

Issue - State: open - Opened by gmalecha about 8 years ago
Labels: refactor

#98 - Modular Types with Higher Kinds

Pull Request - State: open - Opened by gmalecha about 8 years ago - 4 comments
Labels: enhancement

#97 - Set syntax

Pull Request - State: closed - Opened by gmalecha about 8 years ago - 1 comment
Labels: enhancement

#96 - Universe inconsistencies in reification

Issue - State: closed - Opened by gmalecha over 8 years ago - 1 comment
Labels: bug

#95 - Reflected syntax in Set?

Issue - State: closed - Opened by gmalecha over 8 years ago - 1 comment
Labels: question

#94 - Common-code elimination

Issue - State: open - Opened by gmalecha over 8 years ago - 1 comment
Labels: enhancement, refactor

#93 - Try out Coq-style type classes

Issue - State: open - Opened by gmalecha over 8 years ago - 1 comment
Labels: question, performance

#92 - Modular Types + Symbols

Issue - State: open - Opened by gmalecha over 8 years ago - 1 comment

#91 - Clean up the Types Language

Issue - State: open - Opened by gmalecha over 8 years ago - 2 comments
Labels: refactor

#90 - Compilation error with Coq 8.5.2

Issue - State: closed - Opened by clarus over 8 years ago - 2 comments

#89 - Respect COQBIN when calling coq_makefile

Pull Request - State: closed - Opened by JasonGross over 8 years ago - 1 comment

#88 - Polymorphic reification

Issue - State: closed - Opened by gmalecha over 8 years ago - 1 comment
Labels: enhancement, refactor

#87 - Simplify the [rtac] type

Issue - State: closed - Opened by gmalecha almost 9 years ago - 2 comments
Labels: question, performance

#86 - Clean up the Hoare example

Issue - State: open - Opened by gmalecha almost 9 years ago
Labels: documentation

#85 - Clean up Auto example

Issue - State: open - Opened by gmalecha almost 9 years ago
Labels: documentation

#84 - Second-class Polymorphic apply

Issue - State: closed - Opened by gmalecha almost 9 years ago - 1 comment
Labels: enhancement

#83 - Move library of symbols and definitions into Lib directory

Issue - State: closed - Opened by gmalecha almost 9 years ago - 1 comment

#82 - Generic (second-class) polymorphic instantiation for rewriting

Issue - State: closed - Opened by gmalecha almost 9 years ago - 2 comments
Labels: enhancement

#81 - Compilation error with Coq 8.5.0

Issue - State: closed - Opened by clarus almost 9 years ago - 3 comments

#80 - Clean up uses of ExprI.exprD' and Lambda.Expr...exprD'

Issue - State: closed - Opened by gmalecha about 9 years ago - 1 comment
Labels: enhancement, refactor

#79 - Solve universe issues in tests/universes.v

Issue - State: closed - Opened by gmalecha about 9 years ago - 1 comment
Labels: bug

#78 - Make the plugin compatible with the STM

Issue - State: closed - Opened by gmalecha over 9 years ago - 1 comment
Labels: bug

#77 - Reify declarations should be Section-local

Issue - State: closed - Opened by gmalecha over 9 years ago - 1 comment
Labels: bug

#76 - Plugin-based lemma reification

Issue - State: closed - Opened by gmalecha over 9 years ago - 1 comment
Labels: enhancement

#75 - Make rtac and rtacK "opaque-ish"

Issue - State: open - Opened by gmalecha over 9 years ago

#74 - Some references to the removed file ExprUnify.v persist

Issue - State: closed - Opened by ale-f over 9 years ago - 2 comments

#74 - Some references to the removed file ExprUnify.v persist

Issue - State: closed - Opened by ale-f over 9 years ago - 2 comments

#73 - Reification is slow in 8.5

Issue - State: closed - Opened by gmalecha over 9 years ago - 2 comments
Labels: performance

#73 - Reification is slow in 8.5

Issue - State: closed - Opened by gmalecha over 9 years ago - 2 comments
Labels: performance

#72 - Consolidate symAs and funcAs

Issue - State: closed - Opened by gmalecha over 9 years ago - 1 comment
Labels: refactor

#71 - Remove the need for RelDec on Rbase in AutoSetoidRewriteRtac

Issue - State: closed - Opened by gmalecha over 9 years ago
Labels: enhancement

#70 - Sym0, Sym1, ...

Issue - State: closed - Opened by gmalecha almost 10 years ago - 1 comment
Labels: enhancement

#69 - Make it easier to use Rtac syntax

Issue - State: closed - Opened by gmalecha almost 10 years ago - 2 comments
Labels: enhancement

#68 - Rename typX_match_zeta to typX_match_iota

Issue - State: closed - Opened by gmalecha about 10 years ago
Labels: bug

#67 - Optimize APPLY

Issue - State: open - Opened by gmalecha about 10 years ago
Labels: enhancement, performance

#66 - Rtac support runOnGoals_list

Issue - State: closed - Opened by gmalecha about 10 years ago - 1 comment
Labels: enhancement

#65 - Useful lemma

Issue - State: closed - Opened by jldodds about 10 years ago - 1 comment

#64 - Prove the MINIFY tactic

Issue - State: closed - Opened by gmalecha about 10 years ago - 1 comment
Labels: duplicate

#63 - Prove the SIMPLIFY tactic

Issue - State: closed - Opened by gmalecha about 10 years ago

#62 - Way to debug expressions that don't typecheck

Issue - State: open - Opened by jldodds about 10 years ago - 3 comments
Labels: enhancement

#61 - boolean equality for expr?

Issue - State: closed - Opened by jldodds about 10 years ago - 1 comment
Labels: question

#60 - New lemma

Issue - State: closed - Opened by jldodds about 10 years ago - 2 comments

#59 - Minify Proof

Issue - State: closed - Opened by gmalecha about 10 years ago - 1 comment
Labels: bug

#58 - Sanity check values when they pass through [id]

Issue - State: closed - Opened by gmalecha about 10 years ago
Labels: bug

#57 - exprUnify_simul does not have substR

Issue - State: closed - Opened by gmalecha about 10 years ago - 1 comment
Labels: bug

#56 - Unification bug with functions in table

Issue - State: closed - Opened by jldodds about 10 years ago - 1 comment

#55 - Uvar issue with apply/unification

Issue - State: open - Opened by jldodds about 10 years ago - 8 comments
Labels: bug, enhancement

#54 - Only builds under Ocaml 4.01.0

Issue - State: closed - Opened by jldodds about 10 years ago - 5 comments
Labels: wontfix, documentation

#53 - Reification should go under casts

Issue - State: open - Opened by gmalecha about 10 years ago
Labels: bug, enhancement

#52 - Lemmas for applying Rtac

Issue - State: closed - Opened by gmalecha about 10 years ago - 1 comment
Labels: bug

#51 - Errors on let/match

Issue - State: closed - Opened by jldodds about 10 years ago - 9 comments
Labels: bug

#50 - Error reporting in RTac

Issue - State: open - Opened by jldodds about 10 years ago - 4 comments
Labels: enhancement

#49 - Determine a cvb whitelist for exprD'

Issue - State: open - Opened by gmalecha over 10 years ago - 5 comments

#48 - Use [positive] for unification variables (and regular variables?)

Issue - State: open - Opened by gmalecha over 10 years ago - 2 comments

#47 - Move AutoRewrite out of Examples

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: refactor

#46 - Reification should report errors using Coq channels and not throw an anomoly

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: bug

#45 - Reification should backtrack

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: bug

#44 - Install plugin with the install rule

Issue - State: closed - Opened by gmalecha over 10 years ago

#43 - Fix build/build instructions

Issue - State: closed - Opened by jldodds over 10 years ago - 1 comment

#42 - Avoid static linking of reification with coq-plugin-utils

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: enhancement, question

#41 - How difficult would it be to port to trunk?

Issue - State: closed - Opened by gmalecha over 10 years ago - 3 comments
Labels: question

#40 - What does ExprI look like without ts?

Issue - State: closed - Opened by gmalecha over 10 years ago - 2 comments
Labels: question

#39 - What would happen if [Var] and [UVar] were merged?

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: question

#38 - substituteV & sustituteU

Issue - State: closed - Opened by gmalecha over 10 years ago - 3 comments
Labels: enhancement, refactor

#37 - Autorewrite

Issue - State: closed - Opened by gmalecha over 10 years ago - 4 comments
Labels: enhancement

#36 - Typ1 and applications

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment

#35 - Subst Strengthening

Issue - State: closed - Opened by gmalecha over 10 years ago - 2 comments
Labels: wontfix

#34 - STac Match in STac

Issue - State: closed - Opened by gmalecha over 10 years ago - 4 comments
Labels: enhancement, question

#33 - Refactor [mentionsU] and [instantiate] lemmas

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: enhancement

#32 - Convenience Instantiations

Issue - State: closed - Opened by gmalecha over 10 years ago - 2 comments
Labels: refactor

#31 - Proofs in Lambda/ExprSubst

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: bug

#30 - Fix reification framework

Issue - State: closed - Opened by gmalecha over 10 years ago - 8 comments
Labels: bug, enhancement

#29 - Documentation

Issue - State: open - Opened by gmalecha over 10 years ago
Labels: documentation

#28 - Eliminate old interfaces

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment

#27 - Proofs for unification

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: bug

#26 - Hypotheses in STac

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment

#25 - Move Auto out of examples

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: enhancement

#24 - Proofs for FMapSubst

Issue - State: closed - Opened by gmalecha over 10 years ago - 1 comment
Labels: bug

#23 - Mirror-core doesn't seem to build on Windows

Issue - State: closed - Opened by JasonGross over 10 years ago - 8 comments
Labels: bug, documentation

#22 - Consolidate TypesI & TypesI2

Issue - State: closed - Opened by gmalecha over 10 years ago - 2 comments

#21 - Ext & Lambda duplication

Issue - State: closed - Opened by gmalecha over 10 years ago - 2 comments
Labels: wontfix

#20 - Check the performance benefit of using Functors and Modules

Issue - State: open - Opened by gmalecha over 10 years ago - 1 comment
Labels: question, performance, refactor

#19 - Interface for folds?

Issue - State: open - Opened by gmalecha over 10 years ago
Labels: question

#18 - KnotProver

Issue - State: closed - Opened by gmalecha over 10 years ago - 3 comments
Labels: wontfix

#17 - Verify AutoProver2

Issue - State: closed - Opened by gmalecha almost 11 years ago - 2 comments

#16 - Move Iso into ExtLib

Issue - State: closed - Opened by gmalecha almost 11 years ago - 4 comments

#15 - Rework ExprSubst and FMapSubst to factor out common proofs

Issue - State: closed - Opened by gmalecha almost 11 years ago - 1 comment

#14 - Verify FastSubst

Issue - State: open - Opened by gmalecha almost 11 years ago - 1 comment
Labels: wontfix

#13 - Prove Expr_expr is ExprOk

Issue - State: closed - Opened by gmalecha almost 11 years ago - 1 comment
Labels: enhancement

#12 - AutoProver is slow on large problems

Issue - State: closed - Opened by gmalecha almost 11 years ago - 2 comments
Labels: enhancement, performance

#11 - Sketch a guaranteed well-typed Expr implementation

Issue - State: open - Opened by gmalecha almost 11 years ago - 5 comments
Labels: question, performance

#10 - Generalize Prover to work for an arbitrary ILogics

Issue - State: closed - Opened by gmalecha almost 11 years ago - 1 comment

GitHub / gmalecha/mirror-core issues and pull requests