ef36111Merge branch 'master' into repl-definitionsAlyssa Carter12 years ago c578372Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady12 years ago a9dd2e4Lift out proof term into a separate moduleEdwin Brady12 years ago 8f7d848Don't show irrelevant MNs in proverDavid Raymond Christiansen12 years ago ccda94eMerge pull request #1447 from jwiegley/masterDavid Christiansen12 years ago e3be67aBump upper bound on parsers dependencyJohn Wiegley12 years ago 382542aAdd %no_implicit directiveEdwin Brady12 years ago 8407c27Update version numberv0.9.14.1Edwin Brady12 years ago 0c96d97Merge branch 'master' of github.com:idris-lang/Idris-devEdwin Brady12 years ago c72d0f4Split elaborator into multiple source filesEdwin Brady12 years ago 03bf0b1Merge pull request #1444 from david-christiansen/reflection-updatesDavid Christiansen12 years ago 621bd1dMerge pull request #1440 from Melvar/fix-bangbind-opDavid Christiansen12 years ago bc34332Improve quasiquote patterns for MNDavid Raymond Christiansen12 years ago 86a66e1Merge pull request #1443 from david-christiansen/reflection-updatesDavid Christiansen12 years ago e0dc334Update documentation in Language.ReflectionDavid Raymond Christiansen12 years ago bc74895Add Quotable instances for Raw and TacticDavid Raymond Christiansen12 years ago 04e32f5Merge pull request #1414 from Heather/writeLineEdwin Brady12 years ago 8d5c1feMerge pull request #1438 from david-christiansen/reflection-updatesDavid Christiansen12 years ago d10ed5dMerge pull request #1433 from jmitchell/effects-docDavid Christiansen12 years ago a73b6afFix reference to broken primitivesDavid Raymond Christiansen12 years ago 5d25ac8Add regression test for operators starting with "!"Melvar Chen12 years ago 79308e7Add typeclass for programmatic quotingDavid Raymond Christiansen12 years ago 9884992Update Eq and Show reflection for internals changesDavid Raymond Christiansen12 years ago c41b605Update reflection code to current core language.David Raymond Christiansen12 years ago d8bb870Allow “!” to start a larger operatorMelvar Chen12 years ago 5cf623bMerge pull request #1435 from david-christiansen/issue/1434David Christiansen12 years ago 816e85bReinsert check for constructor/family mismatch.David Raymond Christiansen12 years ago 87ac834Add 'doc' and 'doc_clean' make targets for Effects libJake Mitchell12 years ago f0eb9a9Removing an obsolete caseAlyssa Carter12 years ago a114693Instance declarations are working now.Alyssa Carter12 years ago 4d33a16Fixity declarations work in the repl now.Alyssa Carter12 years ago ad81ad3Use a slightly different pretty printer for PDeclsAlyssa Carter12 years ago 0337afeMake proof arguments to list functions implicitDavid Raymond Christiansen12 years ago 92af9baMerge pull request #1425 from david-christiansen/fail-skip-tacticsDavid Christiansen12 years ago 84b172aAdd tactics "skip" and "fail"David Raymond Christiansen12 years ago 481d233rename writeLine to writeString, add writeLineHeather12 years ago 34f63d4Merge remote-tracking branch 'upstream/master' into fix/master/arduinostepcut12 years ago 58eed03Added rts/arudino/idris_main.c. It is similar to the standard idris_main.c except it does not attempt to handle argv/argc and it also calls the Arduino init() function.stepcut12 years ago 4382706If EXIT_SUCCESS and EXIT_FAILURE are not defined (as is the case on Arduino), explicitly define them using standard values (EXIT_SUCCESS == 0, EXIT_FAILURE == 1). In the long term the RTS should be modified to not call exit directly at all since it does not make sense on embedded platforms. The calls to exit(EXIT_SUCCESS) and exit(EXIT_FAILURE). Should be replaced by macros that do something sensible on the platform.stepcut12 years ago 17c887aSet IDRIS_ENABLE_STATS in config.mk instead of in idris_stats.h. stats are not supported on Arduino. Also make sure that when IDRIS_ENABLE_STATS is not set, the idris_stats.h does not pull in time.h as this header is not available on the Arduino platform.stepcut12 years ago